VC Formal 覆盖率分析器 

针对覆盖率收敛的集成形式化分析 

概述
项目越来越依赖覆盖率指标来帮助确定芯片何时准备好流片。然而,并不是总能达到覆盖率目标。VC Formal 覆盖率分析器为使用稳健的形式化技术提供了集成机制,以确定哪个结构覆盖率指标可以达到并且自动排除不能达到的指标。

下载 VC Formal 覆盖率分析器数据手册

针对覆盖率收敛的形式化分析
从获得项目到按时流片需要达到许多签核标准。对于受限随机仿真来说,最重要的要求是覆盖率指标的收敛。覆盖率指标提供了一种方法来衡量仿真测试环境的准确性和完整性。负责验证的专业人士们知道任何具有较差代码覆盖率结果的区域,是因为这些区域还没有经过测试平台测试。对于验证团队来说,这些覆盖率盲区是个危险的信号。然而,下一步操作非常痛苦,即识别哪个未覆盖的目标实际上是能够达到的。某些方面的代码完全是为了极端错误场景而存在的,几乎不可能达到,但是为了正确运行,仍须验证它们。此类区域内的项目覆盖率缺失,就可能是真的盲区,需要改进仿真测试环境。其他方面的代码是由各种操作形成的死代码,程序并不执行这些代码,如重用代码内的未使用功能。可以明显预期到这里会出现覆盖率缺失,因为代码中的这些区域是不能达到的。那么就出现了一个问题,就是需要手动识别哪些代码是可达的。现代验证团队已经与这个问题斗争多年,但是他们遇到了更大的挑战。因为现代芯片的大尺寸和大量的代码重用,都增加了需要排除的不可达代码。这项手动排除过程可能需要数周到数月,这取决于任务的复杂性。

VC Formal 覆盖率分析器通过集成仿真引擎、覆盖率报告和调试解决方案,可自动执行这个耗时费力的过程。这种紧密集成让这个过程变得无缝和易于使用。自动识别与不可达到覆盖项相对的可达到覆盖项,并且提供给验证团队。通过自动化本过程,验证团队可以将精力集中在芯片操作中需要进一步测试的真正可达关键方面,并且轻松地排除那些已经证明不可达的代码。而这一切都要通过形式化验证的功能实现(参考图 1)。


图 1:VC Formal 覆盖率分析器自动识别可达到与不可达到的覆盖率指标

VC Formal 覆盖率分析器
VC Formal 覆盖率分析器将从仿真数据库中提取未覆盖结构覆盖率目标并且正式确定这些目标是否可以达到,这极大地减少了分析代码覆盖率结果所需要的时间。可以更新覆盖率报告来反映实际效果(参见图 2)。


图 2:覆盖率收敛挑战

关键功能与优势
  • 顶级的形式化引擎
    • 经过优化的 VC Formal 覆盖率分析器可以在大型数据库中以最快速度执行分析。
  • 全面的结构覆盖率分析
    • VC Formal 覆盖率分析器自动提取和应用形式不可达性分析到行、条件、toggle 和 FSM 状态转换的覆盖率目标中(参见图 3)。
  • 自动排除和覆盖率指标调整
    • VC Formal 覆盖率分析器生成一个可查看所有不可达到的覆盖率目标的排除文件,可以导入到 VCS® 和 Verdi® ,所以最终覆盖率指标报告可以自动调整,可以和随后的仿真运行一起使用。
独特的价值
  • 行业领先的性能和容量
    • 能够在 RTL 和网表层面的最大型 SoC 设计中有效率地运行。
    • 速度至少比其它工具快两倍,容量高两倍。
  • 易于采用
    • 全面集成 Synopsys VCS 和 Verdi3™ 覆盖率数据库和分析。
  • 卓越的报告、集成和可视化
    • 原生集成 Verdi。


图 3:VC Formal 覆盖率分析器

结论
集成形式化技术在微调仿真结果和帮助项目按时流片方面,具有独特的优势。VC Formal 覆盖率分析器的全面不可达性分析引擎拥有极佳的容量和性能,可在与 Synopsys VCS 和 Verdi 集成的易用流程中执行最大的设计。



NewsArticlesBlogsSuccess StoriesWhite PapersWebinarsVideosTraining Courses