断言竟越复杂越好,最新形式验证工具向丛集级发展

验证工具供应商Real Intent公司的高管日前表示,基于断言的验证已成为市场发展方向,但目前的技术仍然不能满足对全芯片设计进行自动化仿真的要求。为了弥补这方面的缺憾,该公司最近计划推出一款据称技术上有重大突破的静态形式验证工具Conquest。

图:Conquest可以提供丛集级而非模块级的自动验证功能

据Real Intent公司介绍,Conquest可以提供丛集(cluster)级而非模块(block)级的自动验证功能。虽然Conquest并未自称延揽了自动化全芯片验证的圣杯,但就其能够处理更大部分的设计而言,该产品确实“将形式验证沿食物链向上提升了不少,”Real Intent公司行销与业务开发副总裁Rich Farris表示。

“利用Conquest的自动验证构建功能,对模块和丛集级断言的证实过程完全可以实现自动化,就像仿真一样。”Farris说。为了实现全芯片级的验证,他补充道,用户仍然需要一定的工作量,例如调用该工具的迭代指导流程,以此将解决方案导向大多数的复杂断言。

Conquest据称可以自动为多个断言构建证据(proof),可以减轻“假设保证推理”执行的负担,因为“假设保证推理”是手工验证一个个断言时会出现的繁复流程,Real Intent公司首席执行官Prakash Narain表示。他认为,减轻这方面的负担,最终将形成显著的生产率优势 。“这些步骤的自动化对成本降低贡献是非常大的,也是这种(静态形式验证)方法获得成功的必要条件。”Narain表示。

Conquest与面向设计入门阶段应用的一种新型自动化形式验证工具Ascent一起,构成了Real Intent公司EnVision系列新产品的支柱。据该公司透露,Conquest使用了一种正在申请中的专利技术,该技术可以简化对多个复杂断言的证实过程。

历史和常识告诉我们,在基于断言的验证(ABV)中,如果某个复杂断言很难证实,那么证实许多断言将更加困难。但对Conquest来说刚好完全相反,断言越复杂越好。Narain把这个“断言密度悖论”归功于该工具通过证实断言积累设计知识的能力。被证实的断言越多,Narain表示,工具就越了解设计,也就更容易证实进一步的断言。

Conquest还使用标准的ABV语言,并且不依赖矢量质量去检测设计缺陷,Real Intent指出。用户可以利用特殊属性语言(PSL)断言、SystemVerilog断言(SVA)或开放验证库(OVL)检查器,并通过Conquest对设计进行验证,Real Intent公司表示。

另外,在入门级的验证工具方面,Ascent的架构经过了完全重新设计,着重于从RTL获得的自动检查功能。这款工具同样支持PSL和SVA约束的使用,并包含动态仿真链接,Real Intent公司表示。Ascent甚至在可能要仿真之前的设计最初阶段,就能发现RTL代码中的缺陷(bug)。

这两款工具中,每款工具每年的授权费用为3万至10万美元不等。

作者:麦戴伦