65.【SV】SystemVerilog Concurrent Assertions（并发断言）

🔥 SystemVerilog Concurrent Assertions —— 验证工程师的"永不休息的哨兵"

作为芯片验证工程师，不仅要生成激励、收集覆盖率，还要时刻监控设计的行为是否符合预期。SystemVerilog的并发断言就像一个个永不休息的哨兵，它们站在关键信号旁边，在每个时钟节拍检查设计是否违规。一旦发现异常，立刻报告，帮你抓住那些稍纵即逝的bug。

🎯 核心概念：什么是并发断言？

生动比喻

想象你是一个工厂的安全巡检员，你需要检查机器是否正常工作。你可以有两种巡检方式：

并发断言的特点：

• 基于时钟：只在时钟边沿触发检查。
• 采样过去的值：可以引用历史值，比如 $past(signal)。
• 持续监控：一旦启动，在整个仿真期间自动检查。
• 可形式验证：不仅可用于仿真，还可用于静态形式验证。

🔍 一、并发断言的基本语法

一个典型的并发断言长这样：

assert property (@(posedge clk) <布尔表达式>);

• assert property 是断言的关键字。
• @(posedge clk) 指定在时钟上升沿检查。
• <布尔表达式> 是你要检查的条件，它必须为真。如果为假，断言失败。

你也可以给断言起个名字，方便调试：

my_assert: assert property (@(posedge clk) a && b);

📊 二、三个基础例子深度剖析

让我们通过三个逐渐复杂的例子，看看并发断言如何工作。

示例 #1：要求 a 和 b 同时为高

module tb;
bit a, b;
bit clk;

always #10 clk = ~clk; // 产生20ns周期的时钟

initial begin
for (int i = 0; i < 10; i++) begin
@(posedge clk);
a <= $random;
b <= $random;
$display("[%0t] a=%0b b=%0b", $time, a, b);
end
#10 $finish;
end

// 并发断言：在每个时钟上升沿检查 a 和 b 都为1
assert property (@(posedge clk) a & b);
endmodule

关键点：

• 断言在每个时钟上升沿触发，使用当时采样到的值（即上一拍的值，因为非阻塞赋值 <= 在触发沿之后才更新）。
• 如果 a & b 为假，断言失败，仿真器会打印错误信息和位置。

采样机制（非常重要）：

• SystemVerilog 仿真采用调度区域（scheduler regions）模型。在时钟上升沿：
• Preponed 区域：采样所有变量的值（它们在该时刻的值）。这是断言看到的值。
• Observed 区域：评估断言表达式。
• 之后才是非阻塞赋值更新（NBA）区域，将 a <= $random 的值更新到 a 和 b。
• 因此，断言看到的是上一拍的值，而不是刚刚用 <= 赋的新值。这符合大多数协议检查的需求（比如在时钟边沿检查信号是否满足建立时间后的稳定值）。
  

运行结果分析：

断言在 a 或 b 为0的时刻失败，正好符合预期。

示例 #2：要求 a 或 b 至少一个为高

assert property (@(posedge clk) a | b);

module tb;
bit a, b;
bit clk;

always #10 clk = ~clk;

initial begin
for (int i = 0; i < 10; i++) begin
@(posedge clk);
a <= $random;
b <= $random;
$display("[%0t] a=%0b b=%0b", $time, a, b);
end
#10 $finish;
end

// This assertion runs for entire duration of simulation
// Ensure that atleast 1 of the two signals is high on every clk
assert property (@(posedge clk) a | b);

endmodule

这次条件更宽松：只要有一个为1就算通过。

运行结果：

只有第一次两个都为0时失败，其余都通过。这说明断言可以灵活定义规则。

示例 #3：检查 !(!a ^ b) 是否为真

module tb;
bit a, b;
bit clk;

always #10 clk = ~clk;

initial begin
for (int i = 0; i < 10; i++) begin
@(posedge clk);
a <= $random;
b <= $random;
$display("[%0t] a=%0b b=%0b", $time, a, b);
end
#10 $finish;
end

// This assertion runs for entire duration of simulation
// Ensure that atleast 1 of the two signals is high on every clk
assert property (@(posedge clk) !(!a ^ b));

endmodule

这个表达式可以简化一下：!(!a ^ b) 等价于 a ^~ b（即 a 同或 b），但要注意 !a 是对 a 取反，所以实际是 !(~a ^ b)。我们直接按原表达式理解：

真值表（a,b 0/1）：

所以条件在 (a,b)=(0,1) 或 (1,0) 时为真，即 a 和 b 相反时为真。

运行结果：

断言只通过 a≠b 的时刻。这展示了我们可以用复杂的布尔表达式作为属性。

🛠️ 三、并发断言的高级用法

带时序的属性

并发断言的真正威力在于它能描述跨越多个时钟周期的行为。例如：

assert property (@(posedge clk) req |-> ##[1:3] ack);

• 含义：当 req 为高时，在接下来的 1 到 3 个时钟周期内，ack 必须至少一次为高。
• |-> 是蕴含操作符（overlapping implication），表示如果左边成立，右边必须在同一时刻或未来成立（这里 ##[1:3] 表示延迟1-3拍）。

序列（sequence）

可以将一系列事件定义为序列，然后在属性中使用：

sequence s1;
req ##1 gnt;
endsequence

assert property (@(posedge clk) s1 |=> ack);

这里 |=> 表示非重叠蕴含，左边序列结束后下一拍开始检查右边。

调用系统函数

如 $past() 获取过去的值：

assert property (@(posedge clk) $past(valid) && (data == $past(data)+1));

🏢 四、实际验证场景示例

场景1：总线协议握手检查

property handshake;
@(posedge clk) (req && !ack) |=> (ack && !req) ##1 (!ack);
endproperty
assert property (handshake);

检查：请求有效且未应答时，下一拍应答必须有效且请求撤消，再下一拍应答撤消。

场景2：FIFO 满/空标志一致性

property fifo_full;
@(posedge clk) (wr_en && !rd_en && (wr_ptr == rd_ptr–1)) |-> (full == 1);
endproperty

当写使能、读禁止，且写指针将追上读指针时，满标志应为1。

场景3：寄存器写后读回正确

property reg_write_read;
int write_data;
@(posedge clk) (write_en, write_data = data_in) |=> (read_en && read_data == write_data);
endproperty

这里用了局部变量 write_data 捕捉写入值，在下一拍检查读出的值是否一致。

⚠️ 五、常见陷阱与解决方案

陷阱1：采样时机误解

如前所述，并发断言在时钟边沿的 preponed 区域采样，这意味着它看到的是该边沿之前的稳定值。如果你在时钟边沿用阻塞赋值改变信号，断言可能看到旧值，导致误判。

✅ 解决方案：

• 在测试激励中使用非阻塞赋值 <= 驱动信号，使其在时钟边沿后更新，断言看到上一拍的值，符合大多数协议要求。
• 理解调度区域，编写属性时考虑采样时间。

陷阱2：属性过于复杂，难以调试

一个复杂的属性可能长达几行，出错时难以定位。

✅ 解决方案：

• 将复杂属性拆分成多个小属性，分别检查中间条件。
• 给每个属性起有意义的名字，并在失败时打印额外信息（使用 $error 等）。

陷阱3：忘记处理复位

断言在复位期间可能不应检查，否则会误报。

✅ 解决方案：

• 使用 disable iff (reset) 来临时禁用断言：assert property (@(posedge clk) disable iff (rst) req |-> ##[1:3] ack);

陷阱4：属性永远不会失败，但也永远不会成功（空转）

例如，条件 a |-> b 如果 a 从未为真，该属性永远不被触发，既不会成功也不会失败。这可能隐藏问题。

✅ 解决方案：

• 考虑使用覆盖点（cover property）来确保触发条件发生过：cover property (@(posedge clk) req);

陷阱5：并发断言在 initial 块外使用时，必须放在合适的位置

并发断言可以放在 module 内部、interface 或 program 中。如果放在 initial 块内，它只会在 initial 块执行时被评估一次（通常不是我们想要的）。正确的做法是放在 module 的过程块外，这样它从一开始就激活。

✅ 正确示例：

module tb;
// 信号声明
// …
assert property (@(posedge clk) a & b); // 正确位置
endmodule

📈 六、断言结果的处理

断言有几种可能结果：

• 成功：属性被满足。
• 失败：属性被违反。
• 空成功/空失败（vacuous success/failure）：当属性由于前件不成立而自动成功时，称为空成功；当属性被触发但后件失败时，是真正的失败。
• 未决定（在形式验证中）。

仿真器通常会在断言失败时打印信息，我们可以自定义错误信息：

my_assert: assert property (@(posedge clk) a & b)
else $error("a和b不同时为高！");

💎 核心要点总结

验证工程师的心法：

断言是你给设计立下的“规矩”。在写 RTL 的同时，就应该思考哪些行为是必须遵守的，然后把它们写成断言。它们会在仿真中默默守护，一旦有人越界，立刻发出警报。优秀的验证工程师懂得用断言提前捕获 bug，而不是等仿真结束再慢慢分析波形。

最后的小贴士：

• 从简单的布尔断言开始，逐步掌握序列和属性。
• 在关键协议点、状态机跳转、数据通路等处都加上断言。
• 利用覆盖率收集断言触发的次数，确保重要场景真的发生过。
• 记住：断言不仅是检查，也是文档——它们清晰地记录了设计应有的行为。

掌握并发断言，你就拥有了一个永不疲倦的验证助手，24小时监控设计，让 bug 无处遁形！