2. SVA语法入门：序列、属性、断言指令

好，咱们直接进入正题。SVA（SystemVerilog Assertions）说白了就是给硬件写“契约”——你规定信号该怎样跳变，仿真器帮你盯着。我刚开始接触SVA时，觉得它跟Verilog的always块差不多，后来才发现完全不是一回事。

这一节，咱们把三个核心概念讲透：序列（sequence）、属性（property）、断言指令（assert/assume/cover）。这三者层层递进，缺一不可。

2.1 序列（sequence）—— 时序关系的“最小单元”

序列，就是描述信号在一段时间内的跳变关系。你可以把它理解成“时序表达式”。

举个例子：

sequence s1;
  a ##1 b ##2 c;
endsequence

这个序列的意思是：在当前时钟沿，a为高；1拍后b为高；再2拍后c为高。注意，这里的数字是时钟周期数，不是时间。

常用的序列操作符：

操作符	含义	示例
##n	延迟n个时钟周期	a ##2 b
##[m:n]	延迟范围	a ##[1:3] b
$rose(sig)	信号上升沿检测	$rose(clk)
$fell(sig)	信号下降沿检测	$fell(rst)
$stable(sig)	信号保持稳定	$stable(data)
and	两个序列同时满足	s1 and s2
or	两个序列任一满足	s1 or s2
intersect	两个序列同时结束	s1 intersect s2
throughout	条件在整个序列期间成立	en throughout s1
within	一个序列包含在另一个内	s1 within s2

2.2 属性（property）—— 给序列穿上“逻辑外衣”

属性是在序列的基础上，加上逻辑判断条件。说白了，序列只描述“发生了什么”，属性则描述“应该怎样”。

最常用的属性结构：

property p_example;
  @(posedge clk) disable iff (rst)
    antecedent |-> consequent;
endproperty

拆开来看：

• @(posedge clk)：时钟事件，所有采样都在时钟上升沿进行
• disable iff (rst)：当rst有效时，禁用这个属性检查。我习惯把复位条件都写在这里，干净利落
• antecedent |-> consequent：如果antecedent成立，那么consequent必须成立。这是最核心的蕴含操作符

蕴含操作符有两种：

• |->：重叠蕴含。antecedent和consequent在同一个时钟沿判断
• |=> ：非重叠蕴含。antecedent在当前时钟沿判断，consequent在下一个时钟沿判断

举个例子，验证一个简单的握手协议：

property p_handshake;
  @(posedge clk) disable iff (rst)
    $rose(valid) |-> ##[1:3] ready;
endproperty

这个属性说：当valid上升沿到来时，未来1到3拍内ready必须拉高。如果ready在3拍内没拉高，断言就失败。

2.3 断言指令（assert/assume/cover）—— 三种不同的“检查模式”

有了属性和序列，怎么用？三种指令，各有各的用途。

指令	用途	仿真行为	形式验证行为
assert	检查设计行为是否正确	失败时打印错误	作为断言检查
assume	约束输入环境	失败时打印警告	作为约束条件
cover	统计覆盖情况	触发时记录覆盖点	不适用

assert——最常用。用来检查设计是否满足预期。比如：

a_valid_ready: assert property(p_handshake)
  else $error("握手协议失败：valid后3拍内ready未拉高");

assume——约束输入。我在项目中常用assume来限制测试平台的激励。比如：

a_input_stable: assume property(@(posedge clk)
  $stable(data) throughout (valid ##[1:3] ready));

这个assume告诉工具：在valid有效到ready有效的这段时间里，data信号必须保持稳定。如果测试平台违反了，assume会报错。

cover——统计覆盖。用来确认某些场景是否被测试到。比如：

c_handshake_done: cover property(@(posedge clk)
  $rose(valid) ##1 ready);

这个cover统计“valid拉高后正好1拍ready就响应”的情况是否被覆盖到。覆盖率报告里能看到这个cover点触发了多少次。

2.4 实战：一个完整的断言例子

咱们把上面讲的串起来，写一个完整的断言模块：

module assertions_example(input clk, rst, valid, ready, [7:0] data);

  // 序列：valid有效后1~3拍ready响应
  sequence s_handshake;
    valid ##[1:3] ready;
  endsequence

  // 属性：valid上升沿触发握手检查
  property p_handshake;
    @(posedge clk) disable iff (rst)
      $rose(valid) |-> s_handshake;
  endproperty

  // 断言：检查握手协议
  assert_handshake: assert property(p_handshake)
    else $error("Handshake failed at time %0t", $time);

  // 假设：data在握手期间必须稳定
  assume_data_stable: assume property(@(posedge clk) disable iff (rst)
    valid |-> $stable(data) until ready);

  // 覆盖：统计1拍内响应的场景
  cover_fast_handshake: cover property(@(posedge clk) disable iff (rst)
    $rose(valid) ##1 ready);

endmodule

这个例子包含了序列、属性、三种断言指令。你想想看，如果不用SVA，用纯Verilog写同样的检查逻辑，得写多少行？而且可读性差很多。

嗯，这一节的内容就到这里。SVA的语法其实不复杂，难的是怎么把验证思路转化成断言表达式。多写、多仿真、多踩坑，慢慢就有感觉了。