房锐
成都嘉纳海威科技有限责任公司 四川省 610000
摘要: 随着信息技术行业的发展，设计规模和输入数据量的指数性增长,模拟时间已长得无法忍受，另外，也很难判断模拟验证的完备性形式验证不用向量、运用数学方法证明设计的特征和等价性,对这两个问题给出解决办法,但技术发展仍存在不少难题在模拟中引入形式验证技术,形成的断言验证方法,可能是解决验证危机的有效办法。
关键词：数字芯片；断言验证；数学方法
1 形式验证
形式验证是一种系统化方法,用穷举的算法技术证明设计实现满足设计规范的特征,它覆盖了输人的所有可能序列,不需要开发测试向量,检查所有的边角逻辑,提供了完整的覆盖率。
模拟验证中,验证师本人分析设计的特征,找出边角功能然后分析能够激活特征和边角功能的内部状态与外部输入的组合,开发测试实例。并继续模拟,在设计的边界如输出察看是否检测了该特征如果没有,就返回去重新开发测试实例,接着模拟检查许多错误都引入了测试基准,会引入不必要的验证问题而在形式验证里,只要验证师指定设一计特征,由机器应用穷举算法分析设计并进行证明和证伪一验证师摆脱分析和估算激活特征的状态和输人组合以及输出推理的过程验证师放弃设计验证的一些细节,把机械性的重复工作交给推理机器完成,专注于分析指定设计特征,并根据分析结果调整约束显然可以大大提高验证效率形式验证能给出完整覆盖率,应用数学技术分析所有可能的模拟向量,无需逐一模拟,不需要测试实例、但形式验证还不能取代模拟。
1.1等价证明
证明最终网表和原始的RTL设计的等价一直是个问题，一种方法是放弃RTL模型,只用门级模拟作功能验证。另一种是用相同测试集在RTL和门级作模拟,然后比较两者的输出结果显然,用模拟来证明等价是不够的「而且两种方式都会引人模拟瓶颈,延缓项目的上市时间用形式等价证明取代门级模拟,可极大减少验证时间,能提供穷举覆盖率的验证质量。
等价证明用数学方法证明两个设计的逻辑功能是否等价,确保最后的设计实现的功能与寄存器级设计相同。证明时,一般选用规范作为比较标准。等价证明可用来验证从寄存器级到GDSII版图整个芯片设计实现的功能,实际上,在低抽象层次更加有用。
形式等价证明精彩之处在于用符号方式来推理证明或证伪等价性。符号逻辑,在整个输人范围内分析代表逻辑网络的数学表达式,从定义 上讲它就是穷举的。因此只要证明表达式等价性,就证明了在任何输入输 出上 的等价。但等价证明算法非常复杂,无法处理很大的设计。因此必须对设计进行划分以限定问题。一般把设计分割成逻辑锥。逻辑锥是一个逻辑网络,所有的边界都由寄存器、端口或黑盒组成。锥 的概念源于这种逻辑 网络有多个输人一个输出,呈锥子形状。
1.2特征检查
特征检查用数学方法检查设计是否具有给定的特征,如总线控制器不多于一个或者每个发出的信息包都得到了确认。特征比较小,易描述。特征集可以根据设计的进展添加完善。特征检查多用在业务级和寄存器级,这样可以尽早发现错误,以较小代价修正错误。
特征是设计的行为属性,可以是高层属性如网络包的收发特点,或低层属性如有限状态机的状态编码特点。特征一般用来描述设计中的边角逻辑、设计边界或内部模块间的接口协议,有时用来描述复杂的RTL构造。在形式验证里,不用创建测试基准,验证师用一组特征(称为约束)指定合法的输人行为。这组约束是对设计周围环境的抽象,限制形式引擎在合法状态空间中搜索。约束规定设计周围环境的静态行为,如在写周期里双端口存储器的读地址不能等于写地址;和动态行为,如握手协议中模块收到请求信号后,必须在规定的时间内发出恰当的应答信号。没有约束,形式引擎会报告虚假错误,而非设计错误。事实证明,模拟接口断言/约束对于特征检查很重要。
若约束过严,形式引擎就不能发现设计中的错误,也不会给出任何警告信息对约束进行模拟就可以发现问题,任何在模拟时发生冲突的约束,要么RTL错误,要么约束过严在约束限制下,形式引擎穷举搜索设计的合法空间,证明设计特征永远存在,或找到违反特征的激励序列(反例)。
2 断言验证
断言验证就是在模拟中引人形式特征检查的验证方法。用这种方法,设计师编码时插人对特征的描述断言。代码完成后,进行模拟以检查断言,并修改模拟时断言发现的问题。最后,特征检查根据约束限定,穷举搜索设计的状态空间、证明或证伪断言查找设计的错误。很多人感觉到,断言验证将是芯片设计业中下一个突破点,使工程师能继续设计和验证更大更复杂的电路。断言验证,给模拟验证的测试基准和监督技术带来许多非常需要 的技术手段,也有助于普及和接受正在出现的形式验证技术。
最常用的断言定义方法是开放验证库OVL提供的宣称性断言。OVL是基于Veilrog的开放源码的断言监督元件库,以相同方式在RTL中定义静态和动态断言;提供统一的消息报告机制;易于定制;提供一致安全级别,发生严重错误时可停止模拟。由于源码开放,能够根据应用进行定制,因此OVL很吸引人。OVL使用断言模块库,因此在设计中必须实例化断言。目前它还无法定义过程性断言。
以前,仿真的唯一价值是性能。不像模拟,仿真不能让测试基准和监督器监测报告仿真器中的逻辑活动。但现在断言改变了这种情况。利用软硬件有效实现的断言,能在保持仿真性能的同时,提供可观察性、改善仿真的调试能力。但在仿真中运用断言的前提是断言是可综合的。把断言写进设计并综合到FPGA,提高了设计的可观察性,使设计师能够监测结果,一旦有断言冲突就报告。因此当设计放置在快速运行的仿真环境中,就能大大帮助设计师找出设计中残留错误。统一设计和验证的语言正如HDL搭起芯片设计从图形输人到综合的桥梁,解决了设计代沟一样;语言开发对于跨越验证代沟,解决验证危机也非常关键。同样,也需要统一设计和验证的语言来描述今天复杂的设计和测试基准。要求该语言能支持断言描述、高级数据类型、面向对象、并发控制、设计的可观察性、约束性驱动生成和功能覆盖率。把测试基准和断言作为统一语言的一部分,使它们彼此一致,在整个验证中共享通用的语义。这便于模拟引擎直接执行断言检查和形式引擎与模拟引擎的紧密结合。集成环境便于设计师调试设计和断言,也便于采集代码覆盖率和功能覆盖率。采用高级数据类型、并发控制以及面向对象的特性,可提升设计的抽象层次,用更少的代码描述更复杂的可综合设计。另外,面向对象的编程技术比如类、多态性和继承,可以使测试基准逐步集成,以清晰的方式扩展完善。统一的语言描述设计、断言、测试,确保简洁一致的规范、设计和验证描述。
3.结语
芯片产业中出现过两次代沟,设计代沟和验证代沟。设计代沟反映了设计能力和制造能力的落差,通过设计层次上提到寄存器级,HDL和逻辑综合技术大大地改善了设计自动化,成`功地赶上了工艺进步。目前面临的是验证代沟,即验证能力和设计能力的落差。正如设计复用正在帮助缩小设计差距一样,验证复用能够帮助解决验证危机。在设计早期,模块不仅包括设计内容,还应包括一整套的输人生成器、输出检验器和覆盖率工具。测试集应当设计成可移植的,不仅在同一设计的不同抽象层次可移植,还可移植到不同设计中便于模块复用)测试集合应该是层次化的,这样当模块集成到系统级设计时,更高级别的生成器和检验器可用于系统级验证。
参考文献：
[1]Te I, Branson D, Guglielmino E, et al. Pneumatic uscle actuated continuum arms: modelling and experimental assessment. In: 2012 IEEE International Conference n Robotics and Automation (ICRA), Saint Paul, Minnesota, 2012, pp. 4980–4985.
[2]Hkjian GS. Hyper-redundant manipulator dynamics: a ontinuum approximation. Adv Robot 1994;9:217–243.
[3]Yuno F, Sato H. Trajectory tracking control of snake obots based on dynamic model. In: Proceedings of the 2005 EEE International Conference on Robotics and Automation. CRA 2005, Barcelona, Spain, 2005, pp. 3029–3034.