基于自动化验证解决方案的形式验证的容量、性能和广度

自动化针对性解决方案
全自动针对性验证解决方案使验证功能大幅提高，大大节省了工程时间的人月数及昂贵的再流片成本。这实现了对使用其他验证方法难以或无法进行验证特定设计的完整性和验证的准确性。Questa PropGen是该解决方案组合中最新的方案，有助于验证团队通过自动化基于断言的验证（ABV）过程使复杂SoC达到更高质量。



“Mentor的形式验证技术在许多领域增强了我们传统的验证流程，”三星半导体公司系统大规模集成部首席工程师NamDo Kim说。“为了提高生产效率及设计质量，我们已经成功地利用了从全自动形式验证到属性检查的广泛的Questa应用。”



传统上，验证工程师一直依赖于设计人员主动将断言添加至代码中。遗憾的是，编写此类断言所需要的精力和时间往往会阻止设计人员写出验证团队所需的断言。Questa PropGen通过利用其现有测试环境将验证团队视为驾驭者来自动生成属性。项目团队可借助Questa PropGen工具在其SoC仿真和硬件加速环境中体验基于属性的验证（ABV）的所有功能，而无需耗时的手动断言编码。



Questa Formal（形式化验证）引擎的性能和容量的飞跃
Questa Formal独创的新形式验证引擎在棘手验证问题方面提供了业界领先水平的性能。此类引擎为Questa整套产品全自动形式验证解决方案和形式验证强大的应用提供了动力。Questa Formal引擎的增强实现了整个自动化解决方案的性能改进，包括跨时钟域（CDC）签收的业界标准解决方案Questa CDC惊人的6倍提升。为补充全方位验证技术，Questa Formal解决方案和引擎在最近宣布的Mentor 企业级验证平台中还实现了仿真和硬件加速的紧密结合，以便使验证团队能以高水准的质量更有效地实现其总验证目标。



“形式验证正在成为主流，并且技术仍在快速发展，”Oski Technology总裁兼首席执行官VigyanSinghal说，“新发布的Questa Formal引擎所取得的结果给我们留下了深刻印象。在客户项目上，我们已看到大幅提升了容量，拓宽了可解决问题的范围。”