基于OCP的IP内核的自动化形式验证
为了尽可能减少所有这些OCP接口的验证工作量，几家EDA厂商决定创建一个OCP VIP库。这个库(见图3左侧)中包含了OCP一致性计划中定义的所有属性，其代码通常是由一个或多个专业验证工程师采用PSL/SVA+辅助VHDL/Verilog语言编写的。这种代码编写是一次性工作。
图3：厂商提供的库与OCP验证环境的相互作用。
为了选择一组适合某个特定OCP接口的子属性，可以用一个脚本对OCP配置文件(即IP_rtl.conf)进行解析。最终被选出的一组属性可被形式验证工具用作断言或假设。
这个VIP库中还包含了很大的一组cover。这组cover可以检测出过份约束的环境，因此特别重要。此外，cover还能帮助检测到虚警状态(即没有满足条件时出现的断言)，从而可以避免出现无意义的错误。
最后，不要低估开发一套鲁棒性协议VIP的重要性。尽管OCP-IP定义属性的工作做得不错，但在实现时仍可能出现大量问题(例如PCL、辅助Verilog甚至属性子集选择解析器中的错误)。这些问题直接表明一个库必需经过严格测试，在测试阶段，该库被应用于具有不同配置的多个IP。大型EDA厂商通常很适合这一工作，因为他们往往拥有很大的内部IP回归数据库。通常要配合工业客户进行详尽的测试才能完成整个测试过程。
TI提供的一些OCP VIP经验
在TI法国公司的无线终端业务部门(WTBU)，我们可以轻松将Cadence的OCP协议VIP集成到我们内部的设计流程中。必须要定义的(模板)文件只有：
.f: 用于驱动IFV
tcl:用于初始化电路
.psl:用于对非OCP的主要输入(如复位、测试和电源管理)建模
而用户只需要：
· 调用一个Makefile目标对RTL进行分析和详细描述
· 调用一个Makefile目标来解析IP_rtl.conf并获取正确的子集
· 编辑模板文件(.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)，验证工程师既获得了“自由”环境，也得到了“自由”的低层协议检查。
在此基础上，工程师又可以编写更高层次的系统属性。最佳情况下，系统级的属性甚至无需对遗漏的接口(func1 & func2)进行建模就能得到验证。这时的验证更加抽象，因为它是在约束不足的环境下进行的。但如果反例显示出现了有效的违例情况，那么就必须对剩下的接口进行建模。
我们开发的一些最常用的高层属性例子包括：
· 通过桥接进行分组转换
· 存储器和缓存的一致性
· 性能和延迟属性
· 数据完整性(该属性不是很适合形式验证但仍值得一试)
本文小结
采用VIP进行自动化形式协议验证能使关键IP接口得到快速详尽的验证。VIP库在编写和测试之后可用于改善验证质量并缩短验证时间。由于最后的VIP提供了一个“自由”的环境，因而还能用于简化高层系统性能的验证。
友情链接：
