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

　　据Real Intent公司介绍，Conquest可以提供群组(cluster)级而非模块(block)级的自动验证功能。尽管Conquest还未能达成全芯片验证自动化的神圣目标，但就其能够处理更大部份的设计而言，该产品确实已“将形式验证向上提升了不少，”Real Intent公司营销与业务开发副总裁Rich Farris表示。

图：Conquest可提供群组级而非模块级的自动验证功能

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

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

　　 Conquest以及用于设计入门阶段的新型自动化形式验证工具Ascent，两者共同构成了Real Intent公司EnVision系列新产品的支柱。据该公司透露，Conquest使用了一种专利申请中的技术，以简化对多个复杂声明的验证过程。

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

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

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