2. SVA断言基础语法

SystemVerilog Assertion（SVA）的核心价值在于把“设计意图”写成可被仿真器自动检查的时序规则。要写出可综合、可仿真、可复用的断言，必须先把四个基础概念分清：序列（sequence）描述“信号在时间轴上如何出现”，属性（property）描述“在什么条件下必须满足某个序列”，蕴含操作符（|->、|=>）把前提与结论连接起来，时钟采样与复位语义决定断言在哪个时钟沿取值、何时被复位或禁用。本节以 Xcelium 为运行环境，从语法到编译仿真完整走一遍。

一、序列：把时间关系写成表达式

序列是最小的时序描述单元，用 ## 表示时钟周期延迟。例如 req ##1 gnt 表示 req 为高后的下一个采样时钟沿 gnt 为高；##[1:3] 表示延迟 1 到 3 个周期内任意一个周期成立；[*3] 表示连续重复 3 个周期；[->2] 表示“非连续地出现 2 次”。序列本身不产生检查动作，它只是被属性引用的“时间模板”。

sequence s_req_gnt;
  req ##1 gnt;
endsequence

sequence s_burst;
  req ##1 gnt[*3] ##1 done;
endsequence

注意：序列中出现的信号默认在采样时钟沿取值，而不是在信号跳变的瞬间取值。这一点是初学者最容易出错的地方，后文“时钟采样”会专门说明。

二、属性：给序列加上“必须成立”的语义

属性用 property ... endproperty 定义，内部可以包含序列、逻辑表达式、disable iff 复位条件和 not、and、or 等组合。属性必须通过 assert property 实例化后才会被仿真器检查。

property p_req_gnt;
  @(posedge clk) disable iff (!rst_n)
  req |-> ##1 gnt;
endproperty

a_req_gnt: assert property (p_req_gnt)
  else $error("req 拉高后下一拍 gnt 未响应");

这里 @(posedge clk) 指定采样时钟，disable iff (!rst_n) 表示复位有效期间不检查，|-> 是重叠蕴含：前提成立的同一采样沿就开始匹配结论序列。

三、蕴含操作符：|-> 与 |=> 的区别

蕴含是 SVA 最常用的“条件触发”机制，分两种：

• 重叠蕴含 |->：前提成立的那个采样沿，结论序列从同一沿开始匹配。例如 req |-> gnt 要求 req 与 gnt 在同一拍同时为高。
• 非重叠蕴含 |=>：前提成立后的下一个采样沿，结论序列才开始匹配。例如 req |=> gnt 等价于 req |-> ##1 gnt。

如果前提不成立，整个属性默认“空成功”（vacuously true），不会报错。这一点在覆盖率统计中要特别注意：空成功过多说明前提很少被激活，断言实际检查力度不足。

四、时钟采样与复位语义

SVA 采用“采样值”语义：在时钟沿到来前的极小时间窗口（Preponed 区域）对信号取值，断言看到的是沿之前的稳定值，而不是沿之后的新值。因此写 req |=> gnt 时，gnt 是在 req 被采到的下一个沿被采样，而不是同一沿。若把组合逻辑毛刺直接接入断言，可能采到毛刺，通常建议先寄存一拍再断言。

复位语义由 disable iff 控制。它属于异步复位：只要复位条件为真，断言立即被禁用，不产生成功或失败。复位释放后，断言从下一个采样沿重新开始匹配。若复位是同步的，应写成 @(posedge clk) disable iff (!rst_n) 并在复位释放沿之后才开始检查，避免复位释放瞬间的竞争。

五、在 Xcelium 中编译并仿真一个简单断言

下面给出一个可直接运行的最小示例：一个带 req/gnt 握手和异步复位的 DUT，加上一条 req |=> gnt 断言。文件命名为 sva_demo.sv。

module sva_demo(input logic clk, rst_n, req, output logic gnt);
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) gnt <= 1'b0;
    else        gnt <= req;

  property p_req_gnt;
    @(posedge clk) disable iff (!rst_n)
    req |=> gnt;
  endproperty

  a_req_gnt: assert property (p_req_gnt)
    else $error("[SVA] req 后一拍 gnt 未拉高");
endmodule

module tb;
  logic clk = 0, rst_n, req;
  logic gnt;
  sva_demo dut(.clk(clk), .rst_n(rst_n), .req(req), .gnt(gnt));

  always #5 clk = ~clk;

  initial begin
    rst_n = 0; req = 0;
    #22 rst_n = 1;
    #10 req = 1;
    #20 req = 0;
    #40 $finish;
  end
endmodule

编译与仿真命令如下（Xcelium 的 xrun 一步完成编译、精化与仿真）：

xrun -sv -access +rwc sva_demo.sv -top tb -l xrun.log

关键选项说明：-sv 启用 SystemVerilog；-access +rwc 打开读写访问，便于后续波形调试；-top tb 指定顶层；-l xrun.log 把日志写入文件。若断言失败，日志中会出现类似 "sva_demo.sv", 9: tb.dut.a_req_gnt: started at 25ns failed at 35ns 的信息，其中 started 是前提成立的时刻，failed 是结论检查失败的时刻，两者相差一个时钟周期，正好对应 |=> 的语义。

六、常见错误与判断依据

第一类错误是把 |-> 与 |=> 混用。若设计是“req 当拍 gnt 当拍响应”，应写 req |-> gnt；若设计是“下一拍响应”，必须写 req |=> gnt。写错会导致断言在正确设计上误报，或在错误设计上漏报。

第二类错误是复位语义不匹配。若 DUT 使用异步复位，断言必须用 disable iff (!rst_n)；若 DUT 使用同步复位，断言应在时钟沿采样复位，否则复位释放瞬间可能出现假失败。

第三类错误是忽略空成功。若仿真结束断言从未被激活，日志中不会出现失败，但断言实际没有检查任何行为。可通过覆盖点或 $assertcontrol 统计断言激活次数，确认前提确实被激励到。

判断断言是否真正生效，可以看三个证据：编译日志中是否出现断言实例名；仿真日志中是否有 started 记录；波形中前提信号是否确实出现过。三者齐备，才说明这条 SVA 在 Xcelium 中完成了从语法到语义的完整闭环。