对于今天的SoC开发来说,巨大的掩膜制造成本要求首次流片取得成功。急剧增加的验证复杂度与日益缩短的上市时间也敦促业界寻找更加有效和自动化的验证方法。

形式验证(FV)的自动化就是以上问题的一种可行解决方案。作为成熟的伪随机验证技术的补充,FV让验证工程师(或设计师)能够对电路的特定部分进行详尽的验证。本文将讨论OCP等总线协议的自动化形式验证。

属性的概念

为了对任意IP进行形式验证,设计师或验证工程师必需从该IP的规范中提取各种属性。每一种属性描述了该IP的一个或多个特点。最好是先提取高层的系统属性,因为这些属性每个都涵盖了该IP的一组特点。低层的属性接近RTL,因此往往被证明用处不大。

设计师提取出的每一种属性均可以被形式验证工具(例如Cadence的Incisive Formal Verifier)用作断言(检查)或假设(环境约束)。大多数时候,假设被施加到待测设计(DUT)的输入端,断言则被施加于DUT的输出端。例如在OCP协议中有一个属性,它规定应答状态只能在出现相应的请求状态之后启动。在验证带OCP从接口的IP(见图1)时,该属性就被用作断言(检查),因为应答状态是该IP的一个输出。

图1:验证带OCP从接口的IP。

OCP协议的形式验证

在验证带一个或一个以上OCP接口的IP时,理论上只需简单地提取其OCP属性,并对其进行形式上的检验即可,但实际情况并非如此。形式验证中最困难的部分在于OCP规范的复杂性。OCP接口极强的可配置性让我们能够创建一个十分灵活的系统,但同时也加大了验证的负担。确定一组合适的OCP属性非常重要,因为OCP属性的错误选择可能导致一些边界情况被遗漏,从而使验证出现漏洞。

很明显,要求为所有可能的OCP配置确定一组完整的OCP属性列表。OCP-IP组织很早就认识到这一需求。为此,OCP-IP功能验证工作小组(FVWG)创建了一个OCP-IP一致性计划(OCP-IP compliance plan)。该计划对所有OCP属性进行了定义,同时也大致描述了每一个属性应由哪些配置参数激活。同样,在OCP接口配置的基础上,只有相关的一组子属性可以被识别和证实。更全面的描述请参考OCP-IP 2.2规范中的第13、14和15章。

OCP VIP库

今天的许多高性能SoC(例如德州仪器公司的OMAP多媒体应用处理器)都是基于OCP的。在使用时,几个主要器件或主要子系统通过基于OCP的连接与多个从器件(外设和存储器等)相连,见图2。

图2:利用基于OCP的互连实现的内核底层规划。

为了尽可能减少所有这些OCP接口的验证工作量,几家EDA厂商决定创建一个OCP VIP库。这个库(见图3左侧)中包含了OCP一致性计划中定义的所有属性,其代码通常是由一个或多个专业验证工程师采用PSL/SVA+辅助VHDL/Verilog语言编写的。这种代码编写是一次性工作。

图3:厂商提供的库与OCP验证环境的相互作用。

为了选择一组适合某个特定OCP接口的子属性,可以用一个脚本对OCP配置文件(即IP_)进行解析。最终被选出的一组属性可被形式验证工具用作断言或假设。

这个VIP库中还包含了很大的一组cover。这组cover可以检测出过份约束的环境,因此特别重要。此外,cover还能帮助检测到虚警状态(即没有满足条件时出现的断言),从而可以避免出现无意义的错误。

最后,不要低估开发一套鲁棒性协议VIP的重要性。尽管OCP-IP定义属性的工作做得不错,但在实现时仍可能出现大量问题(例如PCL、辅助Verilog甚至属性子集选择解析器中的错误)。这些问题直接表明一个库必需经过严格测试,在测试阶段,该库被应用于具有不同配置的多个IP。大型EDA厂商通常很适合这一工作,因为他们往往拥有很大的内部IP回归数据库。通常要配合工业客户进行详尽的测试才能完成整个测试过程。

TI提供的一些OCP VIP经验

图4:Cadence的OCP协议VIP集成到TI的设计中。

如图4所示,在TI法国公司的无线终端业务部门(WTBU),我们可以轻松将Cadence的OCP协议VIP集成到我们内部的设计流程中。从下图可以看出,必须要定义的(模板)文件只有:

·.f: 用于驱动IFV

·.tcl:用于初始化电路

·.psl:用于对非OCP的主要输入(如复位、测试和电源管理)建模

而用户只需要:

·调用一个Makefile目标对RTL进行分析和详细描述

·调用一个Makefile目标来解析IP_并获取正确的子集

·编辑模板文件(.f/.tcl/.psl)

·最后利用IFV执行形式验证,以检验OCP的一致性

为了让读者对验证流程的简单性与有效性有一个大致的了解,请看以下例子。工程师在验证一个带基本从OCP接口的IP时平均要用30分钟到1个小时的时间。其中大部分时间都用于编写设置主要输入约束的PSL模板文件。需要注意的是,这是100%彻底验证的结果。更加传统的伪随机仿真环境则要求将OCP eVC实例化,编写随机测试用例,最重要的是对功能覆盖率进行严格定义。由于功能覆盖的定义存在一些差异,因此动态回归在OCP接口验证时很可能会遗漏一些边界条件。我们发现在许多模块的动态仿真中常被遗漏的边界条件是,在OCP传输仍未完成时IP就经历软件复位情况下的OCP接口行为。此外,在具备多个OCP接口的模块中,如果一个接口用于配置模块,另一个用于传输实际数据流,那么在采用基于伪随机的仿真方法时也容易出错和留下缺陷。最后一个同时也很难找到的缺陷是FSM死锁,这种缺陷用形式验证的方式比用伪随机仿真的方式更容易发现。

我们在多个无线OMAP项目中采用了OCP VIP方法,每个项目中约有50个IP,每个IP具备一个或一个以上的OCP接口。结果我们发现的问题涵盖了从难以发现的边界条件到结构性缺陷很大的范围。

利用协议VIP进行较高层特性的形式验证

一个IP通常包含:一个clk & rst接口、一个电源管理(PM)接口、一个用于配置其内部寄存器的接口,以及一个或多个用于与外界(串行协议或存储器)通信的功能总线。

对于SoC中常用的标准协议来说,很可能存在相应的协议VIP(OCP,AXI,AHB)。而对于一些内部协议而言,相应的VIP(例如电源管理)也是可以开发的。通过使用这些VIP(见图5),验证工程师既获得了“自由”环境,也得到了“自由”的低层协议检查。

5:协议VIP可以改善验证环境。

在此基础上,工程师又可以编写更高层次的系统属性。最佳情况下,系统级的属性甚至无需对遗漏的接口(func1 & func2)进行建模就能得到验证。这时的验证更加抽象,因为它是在约束不足的环境下进行的。但如果反例显示出现了有效的违例情况,那么就必须对剩下的接口进行建模。

我们开发的一些最常用的高层属性例子包括:

·通过桥接进行分组转换

·存储器和缓存的一致性

·性能和延迟属性

·数据完整性(该属性不是很适合形式验证但仍值得一试)

本文小结

采用VIP进行自动化形式协议验证能使关键IP接口得到快速详尽的验证。VIP库在编写和测试之后可用于改善验证质量并缩短验证时间。由于最后的VIP提供了一个“自由”的环境,因而还能用于简化高层系统性能的验证。

作者:Jeroen Vliegen

WTBU部门形式验证工程师

TI法国公司