原创 基于OCP的IP内核的自动化形式验证

形式验证(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_rtl.conf)进行解析。最终被选出的一组属性可被形式验证工具用作断言或假设。

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

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