在近期举行的设计自动化研讨会(DAC)上，私人控股的EDA供应商Averant公司展位前挂出了一幅含有牙刷和牙线的宣传画，附带的文字说明是“牙刷牙线并用，效果才会最佳。”该公司的高层表示，其寓意是要突出仿真与形式验证之间的关系。该公司认为，设计师需要同时采用这两种技术，才能获得足够的设计收敛。

“你可以把刷牙看成是随机仿真。”Averant公司销售副总裁Larry Lapides说道。就像牙医说笑应该只清洁你想保留的牙齿一样，设计师也应该只对希望取得成功的设计进行静态验证，Lapides指出。

Averant借助DAC的东风，推出了下一代Solidify工具。该工具可以使设计师更好地控制整个形式验证过程。Lapides及Averant公司总裁Ramin Hojati宣称，Solidify 4.0是业界首个经过指导验证的系统，能让设计师在设计周期早期执行快速“缺陷搜寻”操作，稍后再做更彻底的断言检验。

“许多时候设计师会生成成千上成万条特性语句，在一台计算机上需要运行一整晚的时间。”Hojati表示，“设计师有时候也真的想知道某条属性语句是否马上要通过，从而不得不在上面花费很多时间。Solidify工具能让设计师在确定需要花多少时间方面拥有更大的灵活性。”

新工具的增强功能

据Hojati分析，在设计周期早期的缺陷搜寻阶段，用户在一台计算机上处理100条特性语句可能只需数秒时间。稍后当重点转移到全面彻底的检验时，用户可能需要数天和数台计算机才能完成对这些特性的处理。通过有效地权衡完成度与精度和CPU时间之间的关系，Solidify可以提供早期反馈信息，同时尽可能充分地利用可用计算能力，他指出。

Solidify 4.0还包括其它一些增强功能，例如支持完整的SystemVerilog Assertion(SVA)语言。另外也支持在线SVA的使用、通过绑定命令连接的验证知识产权(IP)以及用SVA实现的开放式Verilog库(OVL)，Averant表示。

Hojati和Lapides宣称，Solidify 4.0还提供另外一项业界首创功能：能够在包括SVA、PSL、OVA、OVL和HPL在内的多个特性语言之间进行转换。这样，设计团队就能自由地选择能够最佳地满足他们需要的特性语言，还能实现验证IP的保存与复用。

“Solidify 4.0可以读取四种语言，输出四种语言。”Hojati表示，“这点很有价值。用户可以对他们的IP安全性更加自信。”

其它增强功能包括扩展调试功能和时钟交叉检查以及对1.1版PSL的支持，Averant公司表示。Hojati解释说，扩展调试功能虽然类似于已有的商用调试器，但Solidify能让用户无须转离他们自己的设计环境。

Solidify现在可以在同一设计中处理各种混合的Verilog描述，还支持Liberty的单元格式。Solidify 4.0可以运行在Linux、Windows和Solaris平台。Hojati透露，Averant公司“对产品做了少许的重新配置”，增加了类似于仿真中代码覆盖的特性代码覆盖，据称这是静态验证领域中的独创之举。

Lapides认为，由于人们对形式验证在什么地方适合总体验证方法学有误解，致使形式验证工具市场的发展受到了阻碍。“验证方法学确实在向覆盖验证发展，总体目标是100%的功能覆盖。”Lapides表示，“虽然人们明白缺陷搜寻越早越好，但对于独立工具而言却属于次要价值。”

作者：麦戴伦