VC Formal 

 下一代形式化验证 

概述
SoC 设计的复杂性要求更新、更好的验证方式,以便加速验证和调试,缩短总进度周期,提高进度的可预测性。VC Formal 下一代形式化验证拥有出色的容量、速度和灵活性,可验证某些最艰巨的 SoC 设计挑战,它包括出色的分析、筛选和调试技术,能够快速地找到根本原因。除此之外,在设计进度的早期应用时及仿真可用之前,可以实现整体进度改善(参见图 1)。

VC Formal 数据手册

VC Formal

验证挑战和现代形式化验证
对复杂芯片和系统的验证是一项极具挑战性的任务。工程师和管理层亟需能缩短验证进度、提高可预测性和加速调试的技术。解决此问题的一个方法就是在周期早期尽可能多地识别缺陷。如果较早地捕获缺陷,就能以更低的成本更容易、更快速地分类、调试和修复。但是问题在于要找出难以激励的缺陷是非常困难的,尤其是在看似想象不到的极端状况下。形式化方法就是在这样的情况下诞生的。与其他方法相比,形式化方法减少了依赖用户想出能触发缺陷的潜在场景的情况。当与全球一流调试工具和方法结合使用时,形式化验证的真正威力才得以发挥。

形式方法可以分析独立于或结合仿真的设计,及早发现设计问题,否则在项目进度后期,甚至在生产硅芯片的过程中才察觉到有所遗漏,则变动花费的成本更高,调试也更为困难和耗时。如果在设计周期早期应用,这些方法就可以在仿真测试环境搭建好之前发现 RTL 功能和完备性的问题。

用于下一代形式化验证的 VC Formal
图 1:用于下一代形式化验证的 VC Formal

额外采用形式验证技术可以验证SoC连接的正确性和完备性,并且帮助找出设计RTL不同版本之间的差别。

一旦有了仿真环境,形式验证的方法可以给仿真提供额外的分析来得到更好的结果,比如发现测不到的覆盖率漏洞。

通过在设计和验证方法中适时地运用形式技术,可以在项目中异常轻松地捕获缺陷,这包括难以发现的且直到项目后期才会察觉的未经验证的缺陷。最终能够得到更高质量的设计、改善的总进度以及更强的可预测性。

VC Formal
VC Formal 是一个大容量、高性能的形式化验证解决方案,包含顶级的算法、方法、数据库和用户界面。此解决方案是从头开始构建起来的,旨在解决当今最具挑战性的验证任务,并提供最新和最佳的形式化验证引擎。

关键功能与优势

  • 基于断言的验证
    使用基于形式化证据的技术来验证 SVA 属性或断言,确保跨所有可能的设计活动的正确操作——在仿真环境可用之前就能实现验证。高级的断言可视化和属性浏览、分组和筛选,支持对结果的简单访问。
  • 高级调试
    高级调试接口基于行业标准基于Verdi的 RTL 和波形可视化解决方案构建,包括连接性检查的示意图值注释(参见图 2)

高级调试接口
图 2:高级调试接口

  • 交互性
    实时的断言和约束编辑、证明进展反馈、逻辑锥分析允许用户绝佳的可视性和控制灵活度。(参见图 3)
  • 交互性
    图 3:交互性

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

  • 时序等效性检查
    这允许对设计进行比较,甚至是进行门控功耗电路插入或者微架构修改之后。
  • 形式化覆盖率分析
    作为仿真流程的补充,形式分析技术可以证明覆盖率目标里面没有覆盖的功能点实际上是测试不到的,从而能够在后续的分析中去除它们,节省人力。
  • 时序等效性检查
    图 5:时序等效性检查

  • Certitude 集成
    Certitude 提供用以评估形式化环境的独特信息。与 VC Formal 集成的 Certitude 可以在形式化环境中提供有意义的属性覆盖率指标,并将其作为形式 IP 签发的一部分。同时还可以识别形式环境中的所有不足,例如丢失或错误的属性或约束(参见图 6)。
  • 与 Synopsys 的 Certitude 功能验证系统相集成
    图 6:与 Synopsys 的 Certitude 功能验证系统相集成

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

独特的价值

  • 行业领先的性能和容量

    能够在大设计上高效运行。至少提高 5 倍的性能和容量

  • 易于采用,使用方便

    使用与 Synopsys 实现工具严格一致的模型和命令。VC Formal 脚本看起来就像 Design Compiler® TCL 脚本, 并共享相同的命令和语法。

  • 运行控制功能

    支持网格、暂停/继续、保存/还原

  • 出色的连接性检查功能,包括原理图值注释和根本原因分析

    显著改进的最先进的调试功能,包括对断开网络的调试

  • 引擎分析和控制

    能够跨运行快速检查和控制引擎活动,更好地确保最具挑战性的形式化问题的收敛

结论
采用高级形式化验证技术以改进设计验证的用户正在快速增长。一些特定的验证任务(例如 SoC 连接性验证 和时序等效性检查)的自动化执行显著地加速了技术采用。除此之外,通用的脚本环境和通用设置使得添加启动新形式应用非常简单,如在之前创建的脚本中键入少 数新命令或在 GUI 上一次简单点击。随着符合行业标准的 VCS® 仿真和 Verdi® 调试解决方案的集成,形式化验证发挥了真正的功效。

如需有关 Synopsys 产品、支持服务或培训的更多信息,请访问网站:www.synopsys.com、联系您当地的销售代表或致电 650-584-5000



NewsArticlesBlogsSuccess StoriesWhite PapersWebinarsVideos