DSO.ai
础滨驱动的设计应用
了解更多 →
VC Formal
新一代形式化验证
SoC 设计的复杂性要求快速全面的验证方式，以便加速验证和调试，缩短总进度周期，提高可预测性。VC Formal? 新一代形式化验证解决方案拥有出色的容量、速度和灵活性，可验证某些最艰巨的 SoC 设计挑战，它包括全面的分析和调试技术，能够在 Verdi? 调试平台中快速地找到根本原因。VC Formal 解决方案始终如一地提供更高的性能和容量，发现更多缺陷，针对更大型设计提供更多证据，并通过与 VCS? 功能验证解决方案的本地集成实现更快的覆盖收敛。
VC Formal 解决方案包括一整套正式应用程序 (App)，包括属性验证 (FPV)、自动提取属性 (AEP)、覆盖分析器 (FCA)、连接性检查 (CC)、时序等效性检查 (SEQ)、寄存器验证 (FRV)、测试平台分析仪 (FTA)、形式导航器 (NAV) 以及用于验证标准总线协议的一组断言 IP (AIP）。
功能与优势
- 基于断言的属性验证 (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 覆盖率：先进的技术使形式指标和方法能够实现属性验证签核。