通过形式验证确保您的设计符合主流协议

Cadence® 形式验证 IP (VIP) 经过优化,支持高性能执行和快速调试,由基于断言的 VIP 库组成,用于全面验证被测设计 (DUT) 与特定协议的一致性。利用我们的形式验证 IP,您可以在早期发现关键错误,并缩短整体验证时间。我们所有的形式 VIP 均经过优化,可在我们的形式化引擎和智能资源管理器Jasper™ ProofGrid™中高效执行,同时还可利用我们独特的调试优化器 Jasper QuietTrace™ 进行快速调试。各种 VIP 还可以与我们独特的交互式调试平台 Jasper Visualize™ 配合使用,以尽早整合您的实现和套件和/或快速协议定制/扩展。形式 VIP 包括可重复使用的方法,以探索基于接口事件的协议功能和意图。为支持协议规范的早期探索和验证而生成的协议相关属性,针对形式验证经过了优化,可无缝插入到仿真环境中。

就 Arm® 协议而言,Cadence 所有与 Arm 相关的形式 VIP 产品都经过 Arm 认证,并通过我们的形式化引擎和调试工作流程对性能进行了优化。每个 VIP 产品都可以在我们的 Jasper Formal Property Verification (FPV) 应用上使用,对其内嵌的属性进行形式化证明。因此,您不需要手动编写属性。我们的形式 VIP 产品也可以与许多其他 Jasper 应用一起使用。当形式 VIP 与这些应用一起使用时,您可以通过我们的 Visualize 技术将协议事务和时序图可视化,以了解属性的行为以及设计规范。

形式验证 IP 图
我们的形式验证 IP 可无缝插入 Jasper 应用或仿真环境,帮助您在验证过程中及早发现重大错误

形式 VIP 的主要优点

穷尽验证合规性

用穷尽的基于断言的验证 IP 库来验证设计是否符合标准协议

即插即用

支持自动化、封装式、即插即用功能

提升设计质量

为符合规范的设计提供质量支持

针对形式验证进行优化

针对 Jasper 形式验证平台进行优化

支持领先的仿真器

同时与领先的仿真器兼容,包括 Xcelium™ 逻辑仿真

产品优势

  • 形式 VIP 在 Jasper FPV 应用中使用时调试非常简单,这要归功于功能强大的 Visualize技术显示“实时”有效的波形。如果发现一个反例,可以使用 Visualize 技术即时添加或修改约束。
  • QuietTrace 技术进一步简化了调试过程,计算出描述有关行为所需的最小信号活动,这可以大大加快探索和调试任务。
  • 形式 VIP 产品易于配置,可支持定制和/或只实现一个给定协议的子集的情况。
  • 所有形式 VIP 产品均包括可重复使用的方法,以探索基于接口事件的协议功能和意图。
  • 形式 VIP 中的属性是使用标准的 IEEE SystemVerilog 断言 (SVA) 编写的,并通过我们的形式化引擎对运行时间和内存性能进行优化