等效验证工具在比较两个电路逻辑行为的同时,可确保设计流程的一致性。其目标是将结构性检验用于处理数百万门电路设计。
- 逻辑行为检查
- 分层比较问题
- 有效比较
- 掩盖互连错误
- 网站推荐
Roger B. Hughes
技术推广工程师
Mentor Graphics Corp.
在将等效检验技术应用于大型设计时所出现的问题正变得越来越普遍。任何逻辑等效验证工具的目标都是提供一种满足等效验证的需要的集成解决方案,它可将结构性等效检验的速度与其在微小区域内处理数百万门设计的能力结合起来。
等效检验是多层次形式验证工具的一部分,它包括规则检查和属性检验,它也称为模型检验。这些技术中最难的是规则检查。尽管它已在设计转换综合方面获得了一定的商业成功,但很难集成进现有的设计环境。
属性检验技术在商业上的应用还处在初级阶段。由于通常用于实现属性检验的二进制决策图(BDD)技术所固有的局限性,它并不适合用于整个芯片验证。容量已经成为等效检验技术的一个问题,特别是当设计电路规模超过一百万门时。这已经促使人们感到有必要在验证一个设计时采用分层解剖办法,但这一办法也带来了许多问题,本文稍后将对此做详细说明。
逻辑行为检查
等效验证工具可用来比较两个电路设计的逻辑行为。这些工具确保了设计在整个设计流程中始终保持相同的行为。一个自顶向下的设计流程一般从算法或行为级模型开始,这些模型采用C、Verilog或VHDL等硬件语言进行描述,然后转到更具体的寄存器转换级(RTL)设计,并利用逻辑综合工具实现门级描述。每次一个设计进入到一个新的设计阶段,就有可能引入新的错误。
当从一个设计阶段进入到另一个时,通过比较低一级设计和高一级设计的行为,等效检验工具可让用户发现、诊断和消除无意识引入的错误。即使较小的设计更改(如改变状态机编码或对门级设计重新定时)没有引入任何新的错误,等效验证对于检验而言也是有益的。
在深亚微米系统设计流程的版图设计阶段,等效检验也是很重要的。在布局和物理版图优化之后,电路时序就定下来了,不过人们需要有一种方法来确信在此期间电路功能没有受到影响。在物理版图优化过程中时常发生逻辑变化,因此很重要的一点就是确保这些变化没有改变电路的预期功能。
借助现有的形式验证方法,你无法阅读某种优化工具产生的设计交换格式(DEF)输出,但另外的Verilog输出文件可以描述该设计的功能。因此,对于时序已通过物理布局和优化确定下来的深亚微米设计,可以借助综合生成的网表进行检查(图1)。
图1:效验证在基本设计流程中结合了结构检查
分层比较问题
在分层比较中,有两个成本因素极易被忽略。第一个是与设计分割相关的建立成本,它包括为每一个必须进行的比较指定其环境约束所需付出的开销。不充足的约束可能导致假负结果,即实际上等效的两个设计会表现得并不等效。不准确的约束可能掩盖行为上的实际差异,从而导致假正结果发生。很显然,假负结果越少就越有利于尽快对真正的缺陷进行定位,但假正结果必须绝对避免。
逻辑学家可能会注意到这里所用的假正术语并不严密。严格地说,如果用户指定了约束,那么用户就可以通过对设计环境的简单改变,来消除假正结果。一个真正的假正结果是由于工具引擎掩盖了某个真正的差异而引起的,与两个设计之间的环境无关。
第二个成本因素是由掩盖互连错误而引起的。由于希望一次处理整个设计,再加上处理容量局限,一般不考虑对模块之间互连信号进行检查。因此,设计等效性测试的实现是建立在模块基础上的。这里,最主要的成本因素与模块黑匣子概念有关。以FOO模块(out1、out2、a、b、c)为例,它包含在一个MAIN模块内(Q、QC、X、Y)。如果该FOO模块是黑匣子,那么其顶层模块的新定义就变成MAIN(a、b、c、Q、QC、X、Y、out、out2)。
于是,该FOO的输出就变成了MAIN的附加输入,FOO的输入就变成MAIN的附加输出。这就使得用户可检查所有低一级模块在高一级模块内工作的组合方式。通过用尽一切办法来证明该FOO模块在两种设计中的等效性,最终用户做到了。但遗憾的是,这种情形远没有想像的那么普遍。这种技术仅适用于存储器黑匣子,因为所有输入组合都有可能发生。而对于设计模块,这种方法就不太适用。(图2)示出了有条件等效的例子。
图2:种设计中FOO模块的有条件等效
有效比较
考虑这样一种情景:MAIN提供给FOO的唯一有效的a、b和c组合是(0,0,0)、 (0,0,1)、(0,1,0)、(1,0,0)和(1,1,1)。如果通过考察a、b和c的全部组合来证明该FOO模块在两种设计中的等效性,用户可能发现它们并不等效。然而,在实际设计中由于这种组合数是有限的,因此它们可能完全是等效的。
在低一级模块的输出端可能发生类似的情形。当这些输出作为更高级模块的输入时,必须再次比较所有的组合。例如,当置于实际设计中时,FOO可能刚好产生(0,0)和(1,1) 组合。这对设置有何影响呢？
进行有效比较的唯一途径是将该设计作为一个整体进行比较。如果做不到这一点,就需要了解设计本身的工作原理,以便正确地指定环境约束以避免数以千计的假负结果产生。这绝对是可能的,但却需要用户花费大量的时间来经常做设计验证,并与设计人员交流以确保他们通过环境约束形式正确领会你的设计意图。
出于验证的目的,对任何用于分层分解的工具都要提供所需的数据。简单地进行模块比较是无法进行验证的。这种分层式的验证方法所需的启动费用相当可观。
掩盖互连错误
掩盖互连错误是第二个极为重要的成本因素。
图3:个等效设计P和P'的模块互连
(图3)中,P和P'是两个被认为等效的设计。由于设计常常太大以致于无法进行整个处理,一种常用的方法是按层分割。这种简单的解决办法就是比较A和A',B和B',并指出是否等效。遗憾的是,这将掩盖互连错误。这种方法需要的额外步骤是,将两种设计中的模块A和B进行黑匣处理,并比较BP与BP'。这样,就可观察到互连错误。然而,观察者可能简单地认为这是由黑匣子引起的一个假负结果而忽略它。
对某个设计的分层验证方法从本质上讲,本来就有可能充满各种潜在的人为错误。这已经成为大幅提高各种解决技术的处理能力,和提倡非分层验证方法的一个重要理由。
向大型SoC和ASIC设计的转移,以及与内部和第三方IP的集成已经产生一个仿真瓶颈,这使人们把注意力投向功能验证的形式方法。现代的等效检验工具利用先进的自动化和高效的调试能力可消除这些瓶颈,并可缩短数个星期的验证处理时间,从而大大缩短设计的面市时间。
开放的工业标准Verilog实用(模型)库及用户自定义原型UDP(User Defined Primitive)表的自动综合,均使得用户的集成工作变得更为容易。等效检验可以在整个设计流程中使用,其中包括深亚微米设计的物理版图。在物理优化过程中不经意引入的功能错误可通过一个来自物理优化工具的Verilog输出文件和一个标准.def文件快速地被检测到。先进的调试技术可快速地执行错误比较点的自动分析,并查找出该错误的准确位置。
支持原理图浏览、交叉检查、以及用于检测功能差别的仿真向量生成,极大地提高了生产率,并减少了隔离设计故障源所需的时间。利用当前领先的技术,有可能对32位平台上小于4GB存储器的1500万到2000万门(RTL对网表)各种相关设计进行验证。
传统上,32位结构RAM的理论上限是4GB。利用这项技术,可以在数小时内,在一个32位结构内部处理1500万到2000万门的设计。若设计进一步增大,而又想避免对设计进行分割的话,就需要考虑向64位平台升级。
附栏
FormalPro等效检验器可满足深亚微米设计需求
随着数百万门SoC和ASIC设计复杂性的提高,需要新的技术来满足它带来的验证挑战。等效检验可以在整个设计流程中使用,包括在深亚微米设计的物理版图。在设计流程尾端的物理版图阶段,等效检验显得尤其重要。
设计验证必须快速且严格地执行,而且要确保物理优化过程中的逻辑变化不会影响电路的功能行为。Mentor Graphics公司的FormalPro是专为复杂的等效检验而开发的下一代综合解决方案,可用于设计流程的任一阶段,从RTL直到深亚微米的物理版图优化。
FormalPro可缩短数个星期的验证处理时间,从而大大缩短了设计面市时间。它可以验证在32位平台的存储器容量限制下的1500万到2000万门的各种相关设计。它仅依靠网表执行验证的性能使用户更易于对不同分层进行等效比较。即使分层结构不能保持得象某些深亚微米优化工具所宣称的那样精确,FormalPro也可以很容易地验证各种逻辑变化。
欲了解更多信息,请联系Roger B. Hughes。
E-mail: roger_hughes@; Fax: 1-408-4515766
网站推荐:
掌握用于形式验证的HDL
形式验证有望成为未来设计中的一种基本方法。通过了解RTL描述及其在设计流程中的不同转换可以掌握这项技术。
利用测试基准语言自动化验证过程
专门的验证语言,以及允许你模拟系统描述规范的工具,在复杂芯片和系统的功能性验证中应当起一个重要的作用。
硬/软件协同开发和SoC验证
需要新的工具进行系统级结构规划、硬/软件协同开发、以及目标环境下SoC芯片的完全验证。然而,也需要来自PCB设计领域的许多已被证明的技术。
无线SoC设计的系统验证
本文探讨了面向无线应用的SoC设计的一个关键问题??验证,特别是软硬件协同验证。
京公网安备 11011202001138号
