首页 › 第四篇：效率自动化 App › COV 覆盖率与 UNR

第四章COV 覆盖率与 UNR 不可达分析

第一部分：Coverage App（COV）

概述

Coverage App 度量形式验证的完备性，提供多种覆盖率模型帮助验证工程师了解哪些设计行为已经被验证，哪些还没有。

Coverage Use Models

Coverage App 有三个顶层 use model：Stimuli Coverage、Checker Coverage 和 Bound Coverage。其中 Checker Coverage 又包含 COI、Proof Core、Mutation 三个精度递增的子模型。

覆盖类型说明
Stimuli Coverage在给定约束下判断设计中哪些部分是可达的，用来检查环境的 constrainedness
Checker Coverage度量断言的完备性，下含 COI / Proof Core / Mutation 三级
└ COI Coverage在跑证明之前就能评估属性好不好：求每条属性的影响锥（Cone of Influence），与覆盖模型取交集后报告并集，并报告落在 COI 之外的项
└ Proof Core Coverage跑完证明后，求每个 target 的 proof core 区域（证明所依赖的抽象区域），与覆盖模型取交集，精度高于 COI
└ Mutation Coverage通过对设计注入变异，精确判断哪些元素真正被断言检查到，精度最高（需要 JasperGold Advanced Platform License）
Bound Coverage评估有界证明的质量。有界证明指既没收敛出反例（CEX）也没证明成立、只跑到某个 bound 的证明。Coverage App 会列出该属性 COI 内的 cover item 并按可达 bound 排序，把它们的可达 bound 与属性自身的 bound 对比，就能看出哪些 cover item 需要更大的 bound 才可达，从而判断这个有界证明是否够用。报告字段包括 Assert Bound、In COI、Covered CIs Beyond Bound、Covered CIs Max Bound、Undetermined CIs
使用顺序：精度越高，性能开销越大。官方建议逐级推进——先 COI，再 normal precision 的 Proof Core，然后 high precision 的 Proof Core，最后才用 Mutation。

覆盖率模型

模型说明
Branch Coverage把 RTL 中所有不同的分支枚举为 cover item，为条件构造中每个可能的分支生成一个 cover item。条件构造包括 IF、CASE 和问号表达式（三元运算符）。在 if-else if 级联中，工具会把 else 分支优化掉，并捕获一个空 else 分支
Statement Coverage把 RTL 中不同的语句枚举为 cover item（覆盖 RTL 语句类型的一个子集：IF、阻塞赋值、非阻塞赋值、case、instance）。注意触发条件与仿真不同：仿真中语句的触发条件是构造的敏感列表，而在形式实现中触发条件是逻辑上下文，因此很多语句 cover item 的触发条件恒为 true
Expression Coverage枚举一个逻辑表达式求值为 true 或 false 的各种方式，粒度比 Branch 覆盖率更细。默认纳入分析的 Verilog/SystemVerilog 操作符包括关系类（> >= < <=）和逻辑类（! && || == !=）等
Toggle Coverage度量设计中各信号的活动情况，给出未翻转的信号或保持常量的信号的信息。可用 check_cov -init -toggle_no_ports 避免为模块端口生成 toggle cover item，使一个 net 在层次中只被记分一次
Functional Coverage支持功能覆盖率模型。具体支持的 covergroup 构造见 JasperGold Apps Command Reference Manual 的 "Covergroup Support" 附录，该附录列出对 IEEE Std 1800-2012 covergroup 的支持情况
Coverage App 的 Coverage Analysis 页：按 Formal / Stimuli / Checker 三列显示各信号的覆盖率
Coverage App 的 Coverage Analysis 页：按 Formal / Stimuli / Checker 三列显示各信号的覆盖率

第二部分：UNR App（Coverage Unreachability）

概述

覆盖率不可达分析App 分析仿真覆盖率数据库，形式化证明哪些未覆盖的点是真正不可达的（structural dead code），哪些是因为仿真激励不足而未覆盖的。这可以显著减少覆盖率收敛所需的仿真时间。

支持的覆盖率项

UNR 支持四类覆盖项，在命令中的关键字分别是 block、expr、toggle、fsm：

已知限制：Xcelium 默认不为 VHDL package 统计代码覆盖率，UNR 也不支持在 VHDL package 中生成自动覆盖属性（即使在覆盖配置文件里打开也不行）；若某些块被 formalbuild 优化掉，UNR 也可能无法生成对应的自动覆盖属性。

工作流程

  1. 用 check_unr -init 初始化（必须在 elaborate 之前执行）
  2. 用 check_unr -setup 读入仿真覆盖率数据库并生成覆盖目标
  3. 用 -enable_property / -disable_property 筛选要分析的目标
  4. 用 check_unr -prove 运行证明
  5. 用 check_unr -list 查看哪些未覆盖点被证明为不可达
% check_unr -init -coverage all
% check_unr -setup -coverage {block expr toggle fsm} -covdb test -load_refinement
refine1.vRefine
% check_unr -disable_property .* -regexp
% check_unr -enable_property .*block.* -regexp
% check_unr -list
% check_unr -prove
% database -export_unicov
% check_unr -clear

check_unr 命令详解

顶层子命令共 7 个：-init、-setup、-enable_property、-disable_property、-list、-clear、-prove。各子命令下的常用选项：

子命令常用选项
-init-coverage {block | expr | toggle | fsm}+——生成覆盖目标，须在 elaborate 前调用
-setup-coverage、-task、-covdb <covdb_path>、-dutinst、-load_refinement <refine_files>
-list-type（按状态过滤）、-regexp、-task
-prove-all、-property、-task、-prove_opts、-shallow_analysis（最小努力，1 秒）、-silent、-bg
注意：-covdb 是 -setup 的子选项，不是顶层选项。check_unr 本身没有 -stopat 或 -constraint 选项——stopat 需要在 check_unr -setup 之前单独用 stopat 命令施加，这样覆盖目标生成时才能看到它们；假设（assumption）则在 -setup 前后施加均可，区别在于是否被链接到 UNR task。

-list -type 的状态取值

Embedded Cover Properties 命名

UNR 从仿真覆盖率数据库读取未覆盖的表达式、块、toggle 或 FSM，自动生成断言或 cover，命名规则如下：

Block:      block_cov_line_<number>_<column number>[_Suffix]
            Suffix ::= block<number>[_Suffix]

Expression: expr_cov_line_<number>_<column number>[_Suffix]
            Suffix ::= expr<number>[_Suffix]

Toggle:     toggle_cov_<signal_name>_{fall/rise}[_Suffix]
            Suffix ::= toggle<number>[_Suffix]

FSM:        fsm_cov_reach_<FSM_name>_<state_name>[_Suffix]
            fsm_cov_tran_<FSM_name>_<from_state_name>_<to_state_name>_arc<arcID>[_Suffix]
            Suffix ::= fsm<number>[_Suffix]

覆盖率分析界面

覆盖率分析界面
第 10 页截图
覆盖率分析界面
第 55 页截图
覆盖率分析界面
第 64 页截图

覆盖率闭环方法论

形式覆盖率的意义

形式覆盖率不是仿真覆盖率的替代品，而是补充：

两种"没覆盖到"要分开看

注意这是两个不同 App 里的两个概念，不要混在一张状态表里理解。

UNR App 的属性状态（用 check_unr -list -type 查看）：

状态含义处理
reachable (RCH)形式引擎证明该覆盖点可达仿真激励不足，需要补充测试用例
unreachable (UNR)形式引擎证明该覆盖点不可能到达（dead code）确认是故意的（复位值/常量），否则说明 RTL 有 bug
bounded (BND)UNR 分析未得出确定结论加大努力或增加约束后重跑

Coverage App 的 out-of-COI 报告：这是 COI Coverage 的报告结果，不是 UNR 的状态。COI 覆盖会求出每条属性的影响锥、与覆盖模型取交集，然后既报告落在交集内的项，也报告未被覆盖的项，即 out-of-COI——意思是这些逻辑根本不在任何属性的影响锥内，因此断言不可能检查到它。对应处理是补写覆盖这部分逻辑的属性。Proof Core 覆盖有一个平行的概念叫 out-of-proof-core。

UNR：仿真+形式覆盖率闭环

UNR（Coverage Unreachability）解决仿真验证中的经典问题："仿真没覆盖到，是激励不够还是代码不可达？"

  1. 跑仿真，得到覆盖率数据库（用 -covdb <covdesign>/<covscope>/ 指向该目录）
  2. 未覆盖的覆盖点导入 JasperGold UNR App
  3. 形式引擎对每个未覆盖点证明它是否不可达
  4. 不可达 → dead code，可以从覆盖率目标中排除（在 IMC 中把 unreachable 转成 exclude，GUI 和 batch 模式都支持）
  5. 可达 → 仿真激励不足，需要补充测试用例
价值：UNR 帮你区分"真的需要更多测试"和"代码永远不会执行"，避免在 dead code 上浪费仿真时间。

来源文档

  • jaspergold_cov_userguide.pdf
  • jaspergold_unr_userguide.pdf
  • example_jaspergold_apps/COV/
  • example_jaspergold_apps/UNR/