断言：即时断言与并发断言（SVA 基础）

到目前为止，检查结果对不对靠的都是手写 if (...) $display(...); 这类过程代码。断言（assertion）提供了一种更直接的方式：声明"这个条件应该成立"，工具自动帮你检查，不满足时报告出来。这一章讲两种断言：立即断言（immediate assertion）检查当下这一刻的条件，并发断言（concurrent assertion）检查跨越多个时钟周期的时序关系。

立即断言：像一个内置的检查语句

task automatic check_result(int actual, int expected);
  assert (actual == expected)
    else $error("mismatch: expected=%0d actual=%0d", expected, actual);
endtask

assert (条件) 通过时执行的语句; else 不满足时执行的语句;——else 分支和"通过时的语句"都是可选的。立即断言在程序执行到这一行时立刻求值（就像一条普通语句，在零仿真时间内完成），本质上和 if (!(actual == expected)) $error(...); 做的是同一件事，但写成 assert 更清楚地表达了"这是一处检查点"的意图——而且在真实的工具流程里，断言失败会被单独统计和报告，不会淹没在普通的 $display 输出里。

并发断言：跨越多个时钟周期的时序检查

立即断言只能检查"当下"这一刻的条件；很多验证场景需要检查的是时序关系——比如"某个请求信号拉高之后，几个周期之内必须收到应答"。这正是并发断言的用途，它以时钟为节拍反复采样，检查跨越多个周期的模式：

property req_ack_p;
  @(posedge clk) req |-> ##[1:3] ack;
endproperty
 
assert property (req_ack_p)
  else $error("ack did not follow req within 3 cycles");

拆开来看：

• @(posedge clk)：这个 property 在每个时钟上升沿都会被采样检查一次。
• req |-> ##[1:3] ack：|-> 是"蕴含"操作符，意思是"如果 req 在这个周期为真，那么……"；##[1:3] 表示"未来 1 到 3 个时钟周期之内"。合起来就是"只要 req 为真，ack 必须在之后 1~3 个周期内变为真"——这是协议握手场景里非常典型的检查。

sequence：把时序模式提取出来复用

如果同一个时序模式要在多个 property 里用到，可以用 sequence 把它命名、提取出来：

sequence ack_within_3_cycles;
  ##[1:3] ack;
endsequence
 
property req_ack_p;
  @(posedge clk) req |-> ack_within_3_cycles;
endproperty
 
assert property (req_ack_p)
  else $error("ack did not follow req within 3 cycles");

sequence 描述"一段跨越时间的信号模式"，property 则在 sequence（或普通布尔表达式）的基础上加上蕴含、边沿采样等结构，变成一个可以被 assert property (...) 检查的完整声明。

立即断言 vs. 并发断言：该用哪个

断言是检查器，不是修复手段

断言只负责"发现问题、报告出来"，本身不会改变任何行为——这和第 1 章"设计代码 vs. 验证代码"的心智模型是一致的：断言属于验证的那一半，用来持续检查设计是否符合预期的行为，而不参与实现任何功能。断言回答的是"有没有发生不该发生的事"——一个相关但不同的问题,"该测的场景有没有都测到过",有它自己专门的工具（covergroup）和系统性的方法论，会在 dv-methodology 系列里从头讲起，不在这里展开。

小结

• 立即断言 assert (cond) else ...; 在零仿真时间内检查当下的条件，是 if (!cond) $error(...); 更清晰、更容易被工具单独统计的替代写法。
• 并发断言基于 property，用 @(posedge clk) 按时钟采样，能表达跨越多个周期的时序关系；|-> 表示蕴含，##[m:n] 表示"未来 m 到 n 个周期内"。
• sequence 可以把可复用的时序模式提取出来，供多个 property 引用。
• 断言只检查、不修复，是验证代码（而非设计代码）的一部分。
• 断言回答的是"有没有出错"；另一个工具 covergroup 回答的是"测得够不够"——完整用法，包括语法，留给 dv-methodology 系列展开。