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

推荐给好友

打印

加入收藏

更新于2008-07-23 13:40:12

OCP IP核 自动化 形式验证

         对于今天的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的互连实现的内核底层规划。

文章出处：作者：Jeroen Vliegen WTBU部门形式验证工程师 TI法国公司

分页：1  2