第二章约束环境建模

为什么需要约束

形式验证会穷尽所有可能的输入组合。但在实际设计中，许多输入组合是不合法的（例如协议违规的输入）。如果不约束这些输入，形式验证工具会报告大量虚假的反例（false negative）。

Assume 约束用于定义合法输入空间，告诉工具"输入只会是这样的"。

约束输入

使用 SVA 的 assume property 编写输入约束：

// 示例：假设 valid 信号在 reset 后初始为低
asm_reset_valid: assume property (@(posedge clk) $fell(rstN) |=> !valid);

// 示例：假设 ready 最终会拉高（避免死锁）
asm_ready_eventually: assume property (@(posedge clk) valid |-> s_eventually ready);

// 示例：假设 op 编码只使用 0-3
asm_op_valid: assume property (@(posedge clk) op inside {[0:3]});

黑盒与白盒

黑盒（Black Box）

将某个模块声明为黑盒后，其输出变为自由变量（不受约束），内部逻辑被忽略。这在以下场景有用：

• 模块尚未实现
• 模块是第三方 IP，不需要验证
• 简化证明（移除不相关的复杂逻辑）

# 按模块名黑盒（可重复使用该开关，或用通配符）
elaborate -top top -bbox_m unimplemented_module

# 按实例黑盒
elaborate -top top -bbox_i top.u_pll

# 把缺失模块自动当作黑盒（0 = 缺失模块报错，为默认行为）
elaborate -top top -bbox 1

白盒（White Box）

默认情况下所有模块都是白盒——内部信号和逻辑都可见。JasperGold 可以引用白盒内的任意内部信号用于断言。

初始状态设定

默认情况下，JasperGold 从复位后的状态开始证明。初始状态由 reset 命令的相关开关设定：

# 用一个复位快照文件设定初始状态
reset -init_state <file_name>

# 把不可复位的寄存器初始化为指定常数
reset -expression ~rstN -non_resettable_regs 0

设计复杂度评估

get_design_info 命令输出设计的复杂度指标：

get_design_info

Design Information 用于洞察设计的形式计算复杂度。它提供：

• 结构性指标：端口、寄存器、门的数量等（不带任何参数时返回的就是顶层实例的这组统计；其寄存器数是 flop 与 latch 的总和）
• 功能性指标：计数器集合及其特殊取值、有限状态机集合等
• 对模块和实例，还提供模块源码信息（RTL 行数、实例数、内嵌属性数）和当前 task 信息（当前 task 中的 stopat 数量）

-list 支持在一条命令里给出多个枚举类型，例如 get_design_info -instance myInstance -list output input。常用的枚举包括 flop、latch、gate、register、counter、fsm、fifo、input、output、stopat、bbox_mod、bbox_inst 等。不指定任何参数时，返回顶层实例的信息。

还有一个深度计算用法，可以数出某个信号或属性周围若干层内的寄存器：

get_design_info (-signal <name>+ | -property <name>+) \
                 -list (flop | latch | register) -depth <N> [-boundary]

过约束（Overconstraint）问题

过约束（overconstraint）的准确定义是：施加在设计上的约束缩小了设计的运行模式（即可达状态空间），以致于得到的任何证明都不是完整证明（full proof）。文档把过约束归类为部分证明（partial proof）的两种成因之一——另一种是有界证明（只检查从复位状态起 N 拍以内的 bug）。

过约束与空洞证明（property vacuity）密切相关，但两者定义不同。空洞证明指的是：属性中包含一个 precondition（前提），属性证明通过了，但那个 precondition 因为不可达而从未真正发生。例如在某种配置下 req 根本不可能为 1 时：

// SystemVerilog Assertion
assert property (@(posedge clk) req |=> ack);

这条断言会"证明通过"，但它什么也没验证。工具会在 proven / unreachable 属性的状态旁边显示 vacuity 指示符；当整个 task 被过约束时，同样会看到这个指示符，鼠标悬停可以看到该 task 在第几拍被过约束。

检查过约束的方法：

• 添加 cover 点验证关键场景是否可达
• 使用 check_assumptions 命令理解假设对设计产生的影响：当它找到 CEX 时，会警告你哪些情况可能意味着假设比预期更强，并给出一条 trace 供检查。换句话说，它让你确信自己验证的确实是想验证的东西
• 使用 check_cov -measure 生成覆盖率指标（stimuli、checker、bounded 等），用 check_cov -report 出报告

约束方法论：定义合法的输入空间

约束（assume）是形式验证中最容易被忽视、也是最容易出错的部分。约束决定了形式引擎在什么输入空间内验证设计。

约束的本质

形式引擎会尝试所有可能的输入组合来寻找反例。但在真实芯片中，输入并非完全自由——上游模块、协议规范、物理限制都会限制输入的合法取值。约束的作用就是告诉工具这些限制，让引擎只在合法的输入空间内搜索。

约束过强 vs 约束过弱

约束验证：用 cover 证明约束合理

怎么知道约束是否恰到好处？核心方法是写 cover 属性来"探测"合法场景：

• 如果 cover 击中 → 该场景可达 → 约束没有排除它 ✓
• 如果 cover 不可达 → 要么约束太强把它挡住了，要么设计有 bug

常见约束模式

约束调试技巧

当你看到一个"不合理"的反例时（波形看起来很奇怪）：

1. 检查输入端口的波形——是不是出现了规范不允许的组合？
2. 如果是 → 添加 assume 排除该组合
3. 如果输入看起来合法 → 这可能是真的 bug
4. 对每个新加的 assume，用 cover 确认它没有排除合法场景