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

理解证明状态

调试失败的断言

当断言失败时，JasperGold 会生成一个反例波形（counterexample trace）。这是一个最小长度的输入序列，可以触发属性违反。

反例调试步骤

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

Verification Status Indicators

JasperGold GUI 中使用一系列图标表示验证状态：

• ✅ 绿色对勾：proven
• ❌ 红色叉号：failed
• ⚠️ 黄色三角：bounded（有界证明）
• ⏸️ 灰色方块：not run / unknown
• 🔵 蓝色圆点：covered（覆盖点命中）

处理 Bounded 和 Unknown 属性

增大 Trace Length

set_max_trace_length 100
prove -property <property_name>

切换引擎模式

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

添加抽象

对于复杂设计，可以手动添加抽象（abstraction）来减少状态空间：

# 抽象掉数据路径，只验证控制逻辑
abstract -signal data_bus
# 或使用黑盒
blackbox -module complex_datapath

常见证明问题排查

界面截图

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

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

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

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

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

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

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

🟡 Bounded（黄色）：加深或换引擎

Bounded 证明意味着引擎在当前 trace length 内没有找到反例，但也没有完整证明。处理方式：

• 逐步增大 set_max_trace_length（每次加 20-50）
• 切换引擎：BMC 做有界检查，换 K-Induction（K、N 引擎）尝试完整证明
• 如果加深后转为绿色 → 完成；如果变红 → 反例；如果一直黄色且超时 → 考虑抽象

⚪ Unknown/Timeout（灰色）：复杂度问题

引擎在规定时间内无法确定属性真假，通常是因为设计太复杂。解决思路：

• 增大时间限制：给引擎更多时间（注意 diminishing returns）
• 黑盒化非关键模块：用 -bbox_m 黑盒掉不参与当前属性的子模块
• 添加 cutpoint：在不影响属性的信号上插入 cutpoint 切断状态空间
• 分模块验证：先在块级验证子模块，再到芯片级
• 使用抽象：数据路径抽象（将宽数据路径替换为自由变量）

反例波形调试方法论

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

1. 从波形末尾倒推：找到断言失败的那个时钟周期，看那个周期的信号值
2. 关注红色标记：Visualize 中红色高亮的信号参与了失败路径
3. 使用 Why 分析：右键信号 → Why，自动解释该信号为什么是当前值（展示驱动逻辑）
4. Relevant Logic：自动过滤出与反例相关的信号和逻辑，隐藏无关信号
5. 追踪到输入：从失败点沿着逻辑锥（COI）向前追踪，找到导致错误的根本原因