JasperGold

mart Proof智能验证技术

全新JasperGold平台代表了形式验证技术更新发展阶段，包含不断进步的证明算法和算法混合证明的改善。这一全新平台集成了Smart Proof技术，提升JasperGold中所有应用的验证吞吐率。机器学习技术被用于选择算法并对其参数化配置，实现更高的一次性证明成功率。此外，机器学习也被用于对连续运行的回归测试的优化，无论是运行于本地或者云端。通过使用Smart Proof技术，证明速度可以提高4倍，回归运行速度可以提高6倍。

“在全新的智能JasperGold平台上，我们对我们所有设计案例进行了测试，开箱即用的证明性能提高了2倍，回归运行速度提高了5倍”，STMicroelectronics数字设计验证经理Mirella Negro Marcigaglia说道，“我们也看到没有收敛的Property数量减少了50%以上。综合分析，这些改进大幅提高了我们的验证效率。”

更大的设计规模

当今的SoC设计越来越大、越来越复杂，在进行形式化分析之前，工具的编译能力限制了的所能处理的设计的更大尺寸，并受限于计算资源。升级后的JasperGold平台提供了超过2倍的设计编译容量，与一年前的前代产品相比，编译期间平均内存占用减少50%。此外，工程师可以通过先进的并行编译技术，优化现有计算资源的使用，同时在云端运行证明，有效地增加所能处理的设计规模。

增强形式化Signoff

该平台全新的形式化覆盖技术使工程师可以完全在JasperGold平台内执行IP Signoff。这些新的形式化Signoff技术包括：改进的proof-core精度，利用deep bug hunting技术达到有意义的功能覆盖点，全新形式化覆盖率分析视图。上述特性实现了基于覆盖率的高质量的形式化Signoff，并支持多引擎芯片级验证收敛。

“第一代JasperGold平台在市场上率先推出了商业形式化验证和应用程序，第二代平台则集成了Cadence技术，与主流用户建立起形式化验证的执行流程”，Cadence公司系统和验证事业部 Fabric及形式化解决方案产品线副总裁Ziyad Hanna说，“Cadence第三代智能JasperGold平台显著提升了核心形式化技术，利用机器学习为客户带来切实的性能提升，可应用于更大规模的设计。”

作为Cadence验证套件的组成部分，JasperGold形式化验证平台在vManager™ Metric-Driven Signoff平台环境下提供完整的覆盖率，将JasperGold形式化验证结果与Xcelium™ 仿真和Palladium® 仿真结果指标结合，加快整体验证收敛的速度。该平台是Cadence系统设计实现战略的重要组成，助力系统和半导体公司高效创建完整、差异化的最终产品。Cadence验证套件由一流的JasperGold、Xcelium、Palladium和Protium™ 核心引擎、验证技术和解决方案组成，提高设计质量和吞吐量，满足各种应用程序和垂直产业的验证需求。