第二章证明结果分析与调试

理解证明状态

JasperGold 默认把状态分成两套：运行状态（proof run status）和有效性状态（proof validity status）。先看有效性状态：

状态	含义	下一步操作
`proven` / `covered`	属性已证明 / 覆盖点已命中	✓ 确认属性写对了、约束没过强
`cex`	找到反例（counterexample found）	🔧 分析波形，定位 bug 或补充约束
`unreachable`	覆盖点不可达	🔧 检查是约束过强还是设计问题
`bounded_proven (auto)`	目标深度由工具自动提取，证明深度已达到或超过它	⏫ 如需完整证明，加深或换引擎
`bounded_proven (user)`	目标深度由用户用 `set_prove_target_bound` 指定并已达到	✓ 已满足你自己设定的目标深度
`undetermined`	证明深度小于目标深度	⚙️ 调整引擎、添加抽象、简化属性
`unknown`	初始有效性状态（处理开始之前）	▶️ 还没跑，先跑起来
`error`	属性编译超时，或证明过程发现 task 中的假设与设计、或假设彼此之间不一致	🔧 悬停图标看提示，排查假设冲突

运行状态则是独立的一套：unprocessed（尚未开始证明，无运行状态图标）、queued（排队等待处理）、processing（正在证明）、processed（证明已结束）。证明过程中属性会在 processing 和 queued 之间反复切换，因为引擎在每一轮 proof scan 中会停下又恢复对它们的工作。

三个最容易记错的名字：①断言被违反叫 cex，不叫 "failed"；②有界证明叫 bounded_proven，不叫 "bounded"；③unknown 是"还没开始跑"的初始状态，不是超时——跑了但没收敛是 undetermined，压根没跑是运行状态 unprocessed。

如果在非 expert view 环境下用了 check_sec -prove，Property Table 会退回旧式的单一状态值，此时 Bounded 状态信息不能正确显示。用 set_enhanced_property_status on 可以拿回分离的状态值和 bounded 状态。

调试失败的断言

当断言失败时，JasperGold 会生成一个反例波形（counterexample trace），即一段能触发属性违反的输入序列。

反例不保证是最短的：某些引擎和某些证明设置产生的是非最小（non-minimal）trace。文档明确指出，引擎 J、L、M、N 找到 trace 时"不一定是最短的那条"，引擎 Tri 也可能给出非最小 trace。如果你确实需要最短反例或更强的深度边界信息，用 set_prove_prefer_shortest on——但要注意，只有部分引擎具备在属性已经拿到 cex 或 covered 状态后继续工作的能力（Ht、Bm，以及 check_assumptions 使用的部分引擎），所以必须至少启用其中一个，这个设置才有意义。

反例调试步骤

在 Property Table 中双击 cex 状态的属性
Visualize 窗口自动打开，显示反例波形
追踪波形，找到第一个不满足属性的时钟周期
检查该周期的信号值，确定是设计 bug 还是输入约束缺失
如果是约束缺失，添加 assume 约束后重新证明
如果是设计 bug，修复 RTL 后重新运行

Tracking Signals 确认对话框 — Visualize 的 **Tracking Signals** 确认对话框：追踪某个信号时，工具会问是否把结果作为 results group 直接挂在目标信号下方；勾选 *Save preference and do not show this dialog again* 可以记住选择、不再询问

Verification Status Indicators

Task Tree 顶部的进度条按三种颜色归类有效性状态，鼠标悬停可以看到详细的 validity 和 run 状态信息：

🔴 红色：cex、unreachable、bounded_unreachable (user)
🟢 绿色：proven、covered、bounded_proven (user)
🟡 黄色：unknown、undetermined、bounded_proven (auto)

注意 covered 和 bounded_proven (user) 都归在绿色里，而 unknown 归在黄色里。此外还有一个独立的 vacuity（空洞）指示符，它出现在 proven / unreachable 属性的状态旁边，用来提示这个证明是空洞的——常见诱因有：前提条件 cover 不可达、:live cover 不可达、以及 task 被过约束。

处理 Bounded_proven 和 Undetermined 属性

增大 Trace Length

set_max_trace_length 100
prove -property <property_name>

切换引擎模式

# 尝试不同的引擎组合
set_engine_mode {K I N B L}
prove -property <property_name>

添加抽象

对于复杂设计，可以手动添加抽象（abstraction）来减少状态空间。abstract 命令只有两种抽象形式：

# 计数器抽象：把计数器抽象掉，可指定需要保留的关键值
abstract -counter <signal_name> -values <critical_value>

# 初值抽象：抽象掉指定寄存器的初值（其复位值不再纳入分析）
abstract -init_value <register_name_tcl_list>

# 查看/删除已有的抽象
abstract -counter -list
abstract -counter -remove <signal_name>

被抽象的计数器在 Visualize 窗口中显示为橙色。GUI 路径是 Task – Add Counter Abstraction，对应命令 abstract -counter。

要整块移除逻辑，用黑盒（在 elaborate 阶段指定）或 stopat：

# 按模块名黑盒
elaborate -top top -bbox_m complex_datapath

# 在网表遍历中于某个信号处截断
stopat <signal_name>

常见证明问题排查

问题	可能原因	解决方案
大量 `cex`	缺少输入约束	添加 assume 约束合法输入
所有属性轻易 proven	过约束	添加 cover 点验证可达性
长时间 `undetermined`	状态空间太大	分模块验证、添加抽象、使用 ProofGrid
只拿到有界证明，拿不到完整证明	当前引擎组合里只有"找 trace"的引擎	加入能给出完整证明的引擎，如 M 或 N（B、J、K、L 都只能找 trace / 有界证明）

界面截图

结果诊断方法论：四种结果的决策树

证明完成后，面对 Property Table 中的各种颜色，新手往往不知道接下来该做什么。以下是每种结果的系统化处理方法。

🟢 Proven（绿色）：别着急庆祝

绿色表示引擎在给定约束和深度内证明了属性成立，但在 signoff 之前需要问自己几个问题：

这是我想证明的属性吗？检查属性的自然语言含义，确保 SVA 写的是你真正想验证的东西
约束是否过强？如果约束把输入空间限制得太小，属性可能只是在一个不现实的子空间内成立。用 cover 属性验证：关键合法场景是否能被覆盖到？
是否只是有界证明？bounded_proven 只证明了到某个深度为止成立，不是完整证明。注意 bounded_proven (user) 在进度条里也是绿色，别把它当成完整证明
黑盒是否合理？被黑盒化的模块如果应该参与该属性的逻辑，可能导致假 proven

一个好的实践：对于每个关键断言，写一个对应的 cover 属性来"证伪"约束的合理性。例如断言"grant 始终 one-hot"，可以加 cover "看到四次不同的请求分别被 grant"，确保约束允许所有合法仲裁场景。

🔴 Cex（红色）：分三类排查

红色反例是调试的起点，但不是终点。反例可能来自三种原因，排查顺序很重要：

原因	特征	处理方法
设计 Bug	反例波形中输入完全合法，输出违反了预期协议	修复 RTL，重新 prove
约束缺失	反例波形中输入出现了不合法的组合（如同时要求两个互斥操作）	添加 assume 约束排除非法输入
属性写错	仔细读 SVA，发现断言逻辑本身有误（如用了 \|-> 而不是 \|=>）	修正 SVA，重新 prove

调试顺序建议：先看反例波形中输入信号是否合法。如果输入本身就违反了设计协议（如复位期间就发请求），那是约束问题；如果输入合法但输出错误，那是设计 bug。

🟡 Bounded_proven / Undetermined（黄色）：加深或换引擎

bounded_proven 意味着引擎在当前深度内没有找到反例，但也没有给出完整证明；undetermined 则表示证明深度还没达到目标深度。处理方式：

逐步增大 set_max_trace_length（每次加 20-50）
换成能给出完整证明的引擎：B、J、K、L 这几个引擎的定位就是找 trace 或有界证明——engine B "永远不会给出穷尽证明，只能给出反例或有界证明"，engine K "只搜索 trace，一般不会找到证明"。要拿完整证明，需要 M 或 N 这类"full proof"引擎。N 比 M 对复杂约束的适应性更好，且适合 liveness 属性
引擎之间会交换信息：默认情况下 N 与 C、I、K 在同一属性的证明过程中互通信息，因此 {K I N} 这样的组合是官方示例里就在用的搭配
如果加深后转为绿色 → 完成；如果变红 → 反例；如果一直黄色且超时 → 考虑抽象

🟡 Undetermined（黄色）：复杂度问题

属性跑过了但证明深度始终达不到目标深度，通常是因为设计太复杂。解决思路：

增大时间限制：set_prove_time_limit 设定证明停止前的总时间上限，set_prove_per_property_time_limit 限制每个属性上花的时间
黑盒化非关键模块：用 elaborate -bbox_m 黑盒掉不参与当前属性的子模块
添加 stopat：用 stopat <signal_name> 在网表遍历中于某个信号处截断
分模块验证：先在块级验证子模块，再到芯片级
使用抽象：abstract -counter 抽象计数器、abstract -init_value 抽象寄存器初值

这里说的是 undetermined（跑了但没收敛到目标深度）。如果看到的是 unknown，那说明这些属性还没被处理过——先确认它们真的被 prove 到了。

反例波形调试方法论

当属性失败时，visualize -violation 打开反例波形。高效的调试思路：

从波形末尾倒推：找到断言失败的那个时钟周期，看那个周期的信号值
关注红色标记：Visualize 中红色高亮的信号参与了失败路径
使用 Why 分析：菜单 Tools – Why，或直接双击波形单元格即可运行一次 Why，解释该信号为什么是当前值
Relevant Logic：右键某个"信号-周期"单元格，从上下文菜单选择要高亮的相关逻辑类型。可选项包括 Add Relevant Module Instance Port Signals（只显示目标所在实例的模块端口）、Add Relevant Input/Undriven Signals（只显示主输入和未驱动信号）、Highlight Relevant Logic（执行一次传递性的 Why，遍历 RTL 并高亮 buffer cloud 的两端）。注意它是高亮，不是把无关信号隐藏掉
追踪到输入：从失败点沿着逻辑锥（COI）向前追踪，找到导致错误的根本原因

常见误诊：新手看到红色就去改 RTL，但很多"失败"其实是因为约束不够——工具自由驱动了输入端口，产生了设计规范中不允许的输入组合。先检查反例的输入是否合法！

来源文档

jaspergold_apps_userguide.pdf Appendix B（Verification Status Indicators：Table B-1 运行状态、Table B-2 有效性状态与 vacuity 指示符）
jaspergold_engine_selection.pdf（各引擎能力，以及"trace 不一定最短"的说明）
jaspergold_visualize_gui.pdf（Why、Relevant Logic）
jaspergold_command_reference.pdf（prove / abstract / stopat / elaborate -bbox_m / set_prove_prefer_shortest / set_prove_target_bound）