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

第一部分：Coverage App（COV）

概述

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

Coverage Use Models

覆盖类型	说明
Stimuli Coverage	度量输入激励的覆盖程度
Checker Coverage	度量断言被激活的程度
COI Coverage	度量影响锥（Cone of Influence）内逻辑的覆盖
Proof Core Coverage	度量证明核心的覆盖
Mutation Coverage	变异测试覆盖率（注入变异看能否被检测）
Bound Coverage	有界证明覆盖深度

覆盖率模型

模型	说明
Branch Coverage	分支覆盖率（if/else/case 分支）
Statement Coverage	语句覆盖率
Expression Coverage	表达式覆盖率（条件组合）
Toggle Coverage	翻转覆盖率（信号 0→1 和 1→0）
Functional Coverage	功能覆盖率（cover point 和 cover group）

第二部分：UNR App（Coverage Unreachability）

概述

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

支持的覆盖率项

Block/Statement Coverage
Branch Coverage
Toggle Coverage
Expression Coverage
FSM State/Transition Coverage

工作流程

读取仿真覆盖率数据库（Coverage Database）
指定要分析的未覆盖点
应用 stopats 和约束
运行 check_unr 命令
查看哪些未覆盖点被证明为不可达

# 读取覆盖率数据库
read_coverage_db -sim coverage.ucdb

# 运行 UNR 分析
check_unr -type {block branch toggle}

# 指定 stopats（不关心的信号）
check_unr -stopat {clk reset}

# 应用约束
check_unr -constraint {operation_mode == NORMAL}

`check_unr` 命令详解

Mandatory options（必须选项）：

-type：覆盖率类型
-cov_db：覆盖率数据库

Optional options（可选选项）：

-stopat：不关心的信号列表
-constraint：约束条件
-time_limit：单属性时间限制

Embedded Cover Properties 命名

UNR 自动生成嵌入 cover 属性，命名格式：unr_<type>_<location>。

覆盖率分析界面

覆盖率闭环方法论

形式覆盖率的意义

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

仿真覆盖率告诉你"测试激励覆盖了多少代码"
形式覆盖率告诉你"在穷尽搜索中覆盖了多少状态空间"
两者结合才能完整评估验证进度

Unreachable vs Out-of-COI

分类	含义	处理
Covered	该覆盖点在证明中被击中	——
Unreachable	形式引擎证明该覆盖点不可能到达（dead code）	确认是故意的（复位值/常量），否则说明 RTL 有 bug
Out-of-COI	覆盖点在当前证明的 COI（影响锥）外，属性不涉及该逻辑	添加相关属性或 cover 来覆盖

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

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

跑仿真，得到覆盖率数据库（UCDB/UCIS）
未覆盖的覆盖点导入 JasperGold UNR App
形式引擎对每个未覆盖点证明它是否不可达
不可达 → dead code，可以从覆盖率目标中排除
可达 → 仿真激励不足，需要补充测试用例

价值：UNR 帮你区分"真的需要更多测试"和"代码永远不会执行"，避免在 dead code 上浪费仿真时间。

来源文档

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