第二章约束环境建模

为什么需要约束

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

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

约束输入

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

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

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

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

黑盒与白盒

黑盒（Black Box）

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

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

# 将模块设为黑盒
blackbox -module unimplemented_module

# 将实例设为黑盒
blackbox -instance top.u_pll

白盒（White Box）

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

初始状态设定

默认情况下，JasperGold 从复位后的状态开始证明。可以通过命令自定义初始状态：

# 指定初始状态条件
assume {initial_state} reset_done;

# 设置初始状态值
set_init_state reg_x = 1'b0

设计复杂度评估

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

get_design_info

输出包括：

• 寄存器（flip-flop）数量
• 输入/输出端口数
• 组合逻辑深度
• 估计状态空间大小

过约束（Overconstraint）问题

过约束指假设太强，排除了本应合法的输入行为。过约束会导致属性被 vacuously proven（空洞证明）——在空的输入空间里所有断言都"成立"。

检查过约束的方法：

• 添加 cover 点验证关键场景是否可达
• 使用 check_assumptions 命令检查假设的一致性
• 使用 report_coverage 查看覆盖率

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

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

约束的本质

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

约束过强 vs 约束过弱

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

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

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

常见约束模式

约束调试技巧

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

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