不依赖仿真的“纯”形式验证工具JasperGold问世

新兴的EDA企业Jasper设计自动化公司宣称,它推出的JasperGold产品是一款突破现有容量限制的“纯”形式验证工具,而且该工具非常易于使用。Jasper的前身是Tempus Fugit,为了实现其所谓“规范级”验证的目标,该公司引入了新的管理层、新的投资和新的技术。

在2002年的设计自动化研讨会上,Tepmus Fugit公司曾演示过验证标准接口协议的技术。但JasperGold超越了接口的范畴,承诺能根据高层次的规范级需求以及低层次的声明进行详尽的模块级验证。

“现在,我们才真正起步。” Jasper总裁兼首席执行官Kathryn Kranen表示,“我们正在利用所掌握的标准接口知识,并为工具内建以往具有博士学位的用户才能达到的智能。”她宣称,Jasper的技术是第一次真正的突破,它同时解决了容量和易用性问题。“我们正在捍卫形式验证的荣誉,”她说,“大多数公司不能达到100%彻底验证的目标。”虽然许多供应商已经采用需要使用仿真的“半形式” 验证方法,但Jasper公司认为不依赖仿真的“纯”形式验证才是有前途的方法。

Jasper公司已经引起Gartner Dataquest首席EDA分析师Gary Smith的注意,尽管他对大量公司挤入RTL验证市场一直持怀疑态度。“JasperGold看上去的确是一次突破。”他说,“形式验证是一种非常重要的工具,所以更好的技术在市场中仍有发展的空间。”

不过,一大批老牌EDA公司已经推出形式和半形式工具,包括许多声明和属性检查器。考虑到Jasper的新工具需要一些额外的Verilog编码工作,并需要与用户进行互动,该公司必须在这个过度饱和的市场进行激烈的竞争。

Jasper的技术是基于一种据称可突破容量限制的“预识别引擎”。它之所以能实现这一点,是借助了“状态-空间隧道”技术,该技术引导形式验证引擎只分析与验证每项需求有关的那部分设计。因此,JasperGold不像其它形式工具那样被限制在一个小的验证半径范围内,该公司宣称。

JasperGold是一种交互式工具。它采用“关联指示”(relevance directive),以允许用户指导预识别引擎的工作,这非常类似于底层规划工具对布局和布线的指导。“用户就像在与工具玩游戏,”Tempus Fugit的创始人、现任Jasper公司工程副总裁的Vigyan Singhal形容道,“通过用户与工具之间的互动,工具能更准确地判断从哪里切入设计。”

JasperGold的最大不同之处也许在于它执行规范的能力。“规范可提供比声明更高的抽象级,”Jasper公司首席方法学专家Foster表示,“而且规范能够更完整地定义人们试图要做的事情。”

他指出,规范能够描述端到端(输入到输出)的行为,而声明通常做不到。规范在更高的抽象级描述复杂的行为,而且通常需要额外对行为建模。Foster还发现,规范能同时处理控制路径和数据路径,而声明一般不能检验数据路径。

不过,JasperGold主要用于不执行数据转换或数学运算的模块。“它不适用于DSP的运算部分。”Singhal表示。

JasperGold能处理寄存器传输级(RTL)Verilog代码不超过2万行的模块,Kranen表示。该产品的起价为22.5万美元。Jasper还销售用于众多标准接口的“验证包”,包括PCI、PCI-X、PCI Express、Firewire、ARM Amba、USB、AGP、DDR和千兆位以太网等。Kranen宣称,这是业界最大的形式验证IP(知识产权)库。

要使用JasperGold,设计师首先必须获得用Verilog编写的规范级需求或者从其它语言译出规范级需求。这大约需要在原始设计的基础上增加10%的额外工作量,Kranen表示。但她认为,这比模块级仿真要好得多,因为模块级仿真的测试平台文档规模远远大于原始的Verilog代码。JasperGold的规范需求通常比RTL模块小10倍,她说。

设计师仍需要做系统级仿真,Kranen承认。“这种技术能够验证你是否已经完全清理了模块。它能显著缩短系统仿真的时间。”她说。

JasperGold的运行不是那种只需点击按钮就可以完成的过程。Kranen描述了一个流程:预识别引擎先分析设计,然后返回给用户关于如何消除不相关部分的建议。用户需要提出假设,以帮助工具操纵状态空间。用户还要告诉工具一个给定的波形或事件组合是否合法。

JasperGold将显示规范已经100%地通过验证,或者给出反例的波形。该工具还能产生一个用在仿真中的监视器。它一次只处理一个规范。“它使设计师能创建一个形式测试平台,”Foster表示,“在以前,这基本上是不得不需要一位博士来做的工作。”

作者:葛立伟