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):帮助从形式上验证配置寄存器的行为,如“只读”、“读/写”或“复位值”等相关属性,消除定向测试需求。
  • 具有 Certitude 集成 (FTA) 的形式测试平台分析器:Certitude™ 提供评估形式环境质量的独特能力。与 VC Formal 本地集成的 Certitude 可以提供有意义的属性覆盖率指标,并将其作为形式签发的一部分。同时还可以识别所有不足,例如丢失或错误的属性或约束。与独立故障注入方法相比,本地集成的性能可提高 5-10 倍。
  • 安全验证 (FSV):帮助从形式上验证安全数据不应达到非安全目标,并确保数据完整性,其中非安全数据不应覆盖(或达到)安全目标。
  • 断言 IP (AIP):高性能和优化的断言 IP,用于验证标准总线协议,并可用于 Synopsys VC 形式解决方案和 VCS 仿真。
  • 高级调试和交互性:基于 Unified Verdi GUI 的 RTL 和波形可视化解决方案构建的高级调试界面,包括原理图值注释、动态断言和约束编辑、证明进度反馈以及影响分析锥,可以让用户获得更好的可视性和控制力。
  • 形式化记分板:全面验证数据路径设计的数据完整性。确保通过设计传输的数据未丢失、未重新排序、未损坏以及无重复。
  • Formal 覆盖率:先进的技术使形式指标和方法能够实现属性验证签核。