Cadence推出大众化形式验证工具

为了将形式验证工具扩展到设计师的桌面,Cadence设计系统公司最近推出了Incisive形式验证工具Incisive Formal Verifier。“这是公司首款与一个完整的方法学和流程整合的验证解决方案,”Cadence公司Incisive部产品行销总监Michal Siwinski表示。

Cadence声称,由于新工具允许对RTL代码中的声明进行验证,因此该工具在易用性上达到了一个新的高度。Cadence希望使用其旧款形式验证工具的用户会升级到Incisive Formal Verifier。

Cadence公司迄今为止在形式验证市场上并没有占据太大的份额。根据最新的Dataquest研究报告,明导咨讯公司的0-In工具在2003年的市场占有率为62%,其次是Averant公司的17%和Real Intent公司的15%。由于预测这一市场在未来几年里还将有快速增长,从2003年的990万美元迅速提升到2008年的6680万美元,因此这一市场还有很大的竞争空间。

Siwinski指出,Incisive Formal Verifier的优势在于它的易用性以及客户设计团队对它的快速接受。“形式验证工具过去一直仅在专业从事形式验证的设计师中使用,”他表示,“今天我们采取了一种完全不同的态度。Incisive Formal Verifier是一款适合每一位设计和验证工程师的形式验证工具,它是为大众用户市场开发的。”

形式分析主要用于在验证的早期阶段进行模块级分析。“用户可以在流程一开始就使用形式验证工具,越早使用效果越好。”Siwinski指出。不过,它并不能替代之后的仿真工作。“在未来20年内,当你进入集成设计领域时,市场上不会出现任何一种能够进行全芯片级的形式分析工具。”Siwinski表示。

图1:形式分析加速验证流程

输入到Incisive Formal Verifier的信息包括RTL代码以及属性。这些输入可以被当作声明(验证正确性的属性)或假设(对模块接口进行约束的属性)使用。随着设计确认的难度上了一个台阶,假设变成了需要验证的声明。

Incisive Formal Verifier接受属性规范语言(PSL)、SystemVerilog 声明(SVA)以及开放验证库(OVL)声明。同样的声明可以跨Incisive平台使用,实现仿真、模拟和加速。Incisive工具还可以执行“lint”检查,以确保声明是否有效,并跟踪得到证实的声明。

Incisive工具内含多个形式分析引擎,包括不同类型的二元决定图、自动测试模式生成和SAT解决器引擎等。引擎的选择是自动的,而且对用户来说不可见。一种被称为“假设保证”的功能可以让用户利用已获得验证的声明信息,来确定假设是否已经得到了充分保证。

Incisive工具可以产生三种类型的结果。“通过”表示声明得到了完整的验证；“失败”表示发现了错误,工具会依此产生波形进行调试；如果工具既无法发现错误又无法充分验证某一属性,则会提供一个“验证半径”(proof radius)。在最后这种情况下,用户应该加大范围,重新进行尝试。

Incisive形式验证平台所能够处理的模块大小或属性数量并没有一个绝对数值。Siwinski指出,工具的运行速度依赖于多种因素,但与其它测试基准工具相比,Incisive形式验证平台非常有竞争力。

“更重要的是设计工程师能否获得一个快速的交互环境。”他表示。事实上,声明的验证结果在数秒或数分钟内就会得出,而工程师可以在检查其它属性的同时开始对结果进行调试。

据Siwinski透露,已经有数十家公司开始在生产流程中使用Incisive形式验证平台,其中包括Cadence曾提及的西门子和STMicroelectronics公司。Incisive工具有现货,基于时间许可的一年期费用起价为12万美元。

作者: 葛立伟