📚 课程目录第3章 SVA属性语言核心语法

3. SVA属性语言核心语法

在SoC接口验证中，SVA（SystemVerilog Assertion）的价值不在于“写出一条断言”，而在于用精确的时间语义描述接口协议。一个AXI写地址通道是否在AWVALID拉高后保持稳定直到AWREADY，一个APB传输是否在PSEL有效期间不改变PADDR，这些都需要用序列、属性、蕴含操作符和时钟周期延迟共同表达。本节围绕这四类核心语法，结合局部变量与常用系统函数，说明它们如何落到SoC接口描述中。

序列：描述“一段时间内发生的事件模式”

序列（sequence）用于描述一个或多个时钟周期内成立的事件模式。最基本的序列是单个布尔表达式，例如awvalid；更常见的是用延迟操作符##把多个事件串起来。在SVA中，##n表示“经过n个采样时钟沿之后”，##[m:n]表示延迟在m到n个周期之间任选，##[*]表示零到无穷多周期，##[+]表示至少一个周期。

以AXI写地址握手为例，若要求AWVALID拉高后，在1到3个周期内出现AWREADY，可写成：

sequence aw_handshake;
  awvalid ##[1:3] awready;
endsequence

这里##[1:3]的起点是awvalid被采样为高的那个时钟沿，终点是awready被采样为高的时钟沿。注意，SVA默认在时钟上升沿采样，采样值来自采样时刻之前的稳定值，因此“当前周期”与“下一周期”的边界必须与接口时序图对齐。若把##1误写成##0，就会把同一周期内的两个信号当成先后关系，导致断言在仿真中频繁误报。

属性：把序列组合成可验证的完整断言

属性（property）是比序列更高一层的描述，它可以包含序列、逻辑运算、蕴含和时钟定义。属性本身不是断言，只有通过assert property、assume property或cover property才会被工具检查。一个典型的属性写法如下：

property p_aw_handshake;
  @(posedge clk) disable iff (!rst_n)
  awvalid |-> ##[1:3] awready;
endproperty

a_aw_handshake: assert property (p_aw_handshake);

其中@(posedge clk)定义了采样时钟，disable iff (!rst_n)表示复位有效期间不检查该属性。属性可以复用，也可以嵌套调用其他序列或属性，这在SoC接口验证中非常关键：同一套握手属性可以复用于多个主从端口，只需替换信号名或通过参数化模块传入。

蕴含操作符：区分“触发条件”与“必须结果”

蕴含操作符是SVA中最容易用错、也最能体现协议意图的部分。它分为两类：重叠蕴含|->和非重叠蕴含|=>。两者的区别在于：|->要求后续序列从当前周期开始匹配，|=>要求后续序列从下一个周期开始匹配。

例如，要求“只要AWVALID为高，则同周期内AWADDR必须稳定”，应使用重叠蕴含：

awvalid |-> $stable(awaddr)

而要求“AWVALID为高后，下一周期AWREADY必须为高”，则应使用非重叠蕴含：

awvalid |=> awready

如果误用|->表达“下一周期”，断言会提前一个周期检查，造成漏报或误报。另一个常见问题是“先行算子”不成立时的空成功：当awvalid为低时，awvalid |-> ...自动成功，这并不代表协议被验证了。因此，在覆盖关键握手时，通常还要配合cover property确认先行条件确实被触发过。

时钟周期延迟与局部变量：让属性具备“记忆”

局部变量（local variable）允许在序列匹配过程中捕获某个时刻的采样值，并在后续周期中比较。这在SoC接口中非常实用，例如检查“写地址发出后，写数据必须与地址对齐”或“同一笔传输的ID保持不变”。

property p_awid_stable;
  logic [3:0] id;
  @(posedge clk) disable iff (!rst_n)
  (awvalid, id = awid) |-> ##[1:5] (awvalid && awid == id);
endproperty

这里(awvalid, id = awid)是带局部变量赋值的序列，它在awvalid为高的周期把awid存入id，然后在后续1到5个周期内检查awid是否仍等于该值。局部变量必须注意作用域和赋值时机：赋值发生在序列匹配的当前采样周期，后续比较使用的是采样值，而不是仿真时间上的连续值。

与延迟相关的常用系统函数还包括$past、$rose、$fell、$stable和$changed。$past(sig, n)返回n个周期前的采样值，$rose(sig)表示当前周期为1且上一周期为0。例如，检查PSEL上升沿后PENABLE不能立即为高，可写成：

$rose(psel) |-> ##1 !penable

这些函数让属性不必显式展开多个周期，也能表达边沿和保持关系。但要注意，$past在仿真开始阶段可能返回未知值，因此通常配合disable iff或$isunknown做保护。

在SoC接口描述中的组合应用

把上述语法组合起来，可以形成一条完整的接口属性。以APB写传输为例，要求：PSEL拉高后，PADDR和PWRITE在PENABLE有效前保持不变，且PENABLE必须在PSEL之后一个周期拉高。可写成：

property p_apb_write;
  @(posedge clk) disable iff (!presetn)
  $rose(psel) |-> ##1 penable && $stable(paddr) && $stable(pwrite);
endproperty

这条属性同时用到了边沿函数、非重叠蕴含、时钟周期延迟和稳定函数。若仿真中该属性失败，波形上通常能看到penable没有在psel后一个周期拉高，或者paddr在penable前发生了跳变。此时应回到接口时序图，确认##1的参照沿是否正确，以及$stable的采样窗口是否覆盖了协议要求的保持区间。

常见误用与检查要点

第一，延迟基准混淆。##1表示“下一个采样周期”，不是“1纳秒”或“1个仿真时间单位”。在SoC接口中，若时钟频率为200MHz，一个周期为5ns，但SVA只关心采样沿，不关心绝对时间。第二，重叠与非重叠混用。检查“同周期稳定”用|->，检查“下一周期响应”用|=>，两者不可互换。第三，局部变量赋值时机错误。局部变量在序列匹配的当前采样周期赋值，后续比较使用采样值，若在赋值前就引用，会得到未初始化值。第四，忽略复位保护。未加disable iff的属性在复位释放瞬间可能因信号未知而失败，应结合$isunknown或复位条件过滤。

实际调试时，建议先单独运行cover property确认先行条件被触发，再打开assert property检查结果。若断言失败，优先查看波形中先行算子成立的时刻、后续序列的采样沿位置以及局部变量捕获值，而不是直接修改延迟参数。只有把序列、属性、蕴含、延迟和局部变量放在同一张时序图上核对，才能让SVA真正成为SoC接口协议的可执行描述。