VC Formal

功能与优势

• 基于断言的属性验证 (FPV)：使用基于形式化证据的技术来验证 SystemVerilog 断言 (SVA) 属性，确保跨所有可能的设计活动的正确操作，在仿真环境可用之前就能实现验证。高级的断言可视化、属性浏览、分组和筛选，支持对结果的简单访问。

• 自动提取属性检查 (AEP)：自动功能分析，用于出界数组、算术溢出、X 分配、同时设置/重置、完全案例、并行情况、多驱动器/冲突总线和浮动总线检查，无需专门的测试。

• Formal 覆盖率分析 (FCA)：作为对仿真流程的补充，VC Formal 提供的证据表明，覆盖目标中的未覆盖点实际上是不可达到的，从而可以将它们从后续分析中移除，节省大量的人力。

• SoC 级连接性检查 (CC)：SoC 级的连接性验证。灵活的输入格式易于集成。强大的调试能力，包括值注释、原理图查看、源代码浏览和分析报告速度分析。自动分析未连接的连接性检查的根本原因，可以大大节省调试时间。

• 时序等效性检查 (SEQ)：此功能可以比较设计，在寄存器重定时之后，插入用于功耗优化或微架构更改的门控时钟。

• 形式导航器 (HAB)：仅使用统一 Verdi GUI 中的 RTL 设计（使用/不使用断言或测试平台）启用调试和“假设分析”。

• 寄存器验证 (FRV)：帮助从形式上验证配置寄存器的行为，如“只读”、“读/写”或“复位值”等相关属性，消除定向测试需求。

• 具有 Testbench Quality Assurance 集成 (FTA) 的形式测试平台分析器：Testbench Quality Assurance 提供评估形式环境质量的独特能力。与 VC Formal 本地集成的 Testbench Quality Assurance 可以提供有意义的属性覆盖率指标，并将其作为形式签发的一部分。同时还可以识别所有不足，例如丢失或错误的属性或约束。与独立故障注入方法相比，本地集成的性能可提高 5-10 倍。

• 安全验证 (FSV)：帮助从形式上验证安全数据不应达到非安全目标，并确保数据完整性，其中非安全数据不应覆盖（或达到）安全目标。

• 断言 IP (AIP)：高性能和优化的断言 IP，用于验证标准总线协议，并可用于 Synopsys VC 形式解决方案和 VCS 仿真。

• 高级调试和交互性：基于 Unified Verdi GUI 的 RTL 和波形可视化解决方案构建的高级调试界面，包括原理图值注释、动态断言和约束编辑、证明进度反馈以及影响分析锥，可以让用户获得更好的可视性和控制力。

• 形式化记分板：全面验证数据路径设计的数据完整性。确保通过设计传输的数据未丢失、未重新排序、未损坏以及无重复。

• Formal 覆盖率：先进的技术使形式指标和方法能够实现属性验证签核。