2. SVA语法入门：SVA的基本结构、序列与属性的定义

各位同学，咱们今天聊聊SVA的语法基础。说实话，我刚接触SVA那会儿，看着满屏的|->和##符号，头都是大的。但后来我发现，这东西说白了就三个核心概念：序列（sequence）、属性（property）和断言（assert）。搞懂这三者的关系，SVA就入门了。

2.1 SVA的基本结构：三层架构

我个人习惯把SVA理解成一个「三层汉堡」：

底层：序列（sequence）——描述信号在时钟边沿上的行为模式
中层：属性（property）——把序列组合成逻辑判断条件
顶层：断言（assert/cover/assume）——告诉工具你要检查什么

你想想看，这不就跟写C语言一样吗？先定义变量（序列），再写函数（属性），最后调用（断言）。

核心公式：

sequence + property + assert = 完整的SVA检查

2.2 序列（sequence）的定义

序列是SVA的最小单元。它描述的是「信号在连续时钟周期里的变化」。我举个例子：

// 最简单的序列：信号a在时钟上升沿为高
sequence s_a_high;
    @(posedge clk) a;
endsequence

// 带时序的序列：a拉高后，下一周期b拉高
sequence s_a_then_b;
    @(posedge clk) a ##1 b;
endsequence

// 带重复的序列：a连续拉高3个周期
sequence s_a_repeat3;
    @(posedge clk) a[*3];
endsequence

这里有几个关键操作符，我列个表方便你对照：

操作符	含义	示例	说明
`##n`	延迟n个时钟周期	`a ##2 b`	a拉高后，过2个周期b拉高
`[*n]`	重复n次	`a[*3]`	a连续拉高3个周期
`[->n]`	非连续重复n次	`a[->3]`	a总共拉高3次，中间可以隔周期
`and`	两个序列同时结束	`s1 and s2`	s1和s2必须在同一周期结束
`or`	两个序列任一结束	`s1 or s2`	s1或s2任意一个结束即匹配
`intersect`	两个序列长度相同且同时结束	`s1 intersect s2`	比and更严格，长度必须一致

我的小经验：刚开始写序列时，##n的n值最容易搞错。我建议你画个波形图，数清楚时钟沿再写代码。我在项目中吃过这个亏——少写了一个##，仿真跑了三天才发现问题。

2.3 属性（property）的定义

属性是序列的「逻辑外壳」。它给序列加上了触发条件和检查方向。说白了，序列只告诉你「发生了什么」，属性告诉你「应该发生什么」。

// 基本属性结构
property p_name;
    @(posedge clk)
    disable iff (rst)    // 复位时禁用检查
    start_event |-> sequence_body;
endproperty

这里最核心的是蕴含操作符：

|->：重叠蕴含（antecedent和consequent在同一周期开始检查）
|=>：非重叠蕴含（antecedent结束后下一周期开始检查consequent）

我画个图帮你理解：

嗯，这里要注意：disable iff一定要加。我曾经在一个项目中忘了写复位条件，结果仿真一复位，断言疯狂报错，整个log文件几十万行。从那以后，我写属性第一件事就是加disable iff (rst)。

2.4 完整的断言示例

把序列和属性组合起来，就是一个完整的断言：

// 场景：当req拉高时，2个周期后ack必须拉高
module check_handshake;

    logic clk, rst, req, ack;

    // 定义序列
    sequence s_req;
        @(posedge clk) req;
    endsequence

    sequence s_ack_delayed;
        @(posedge clk) ##2 ack;
    endsequence

    // 定义属性
    property p_req_ack;
        @(posedge clk)
        disable iff (rst)
        s_req |-> s_ack_delayed;
    endproperty

    // 断言检查
    assert property (p_req_ack)
        else $error("req没有在2周期后得到ack响应");

    // 覆盖率收集
    cover property (p_req_ack);

endmodule

我曾经踩过的坑：

序列里忘记加时钟@(posedge clk)——仿真直接报语法错误
##2和##[1:3]搞混——前者是精确延迟2周期，后者是1到3周期范围
属性里用了|->但实际需要|=>——检查时序差了整整一个周期

2.5 序列的复用与参数化

实际项目中，同一个序列可能被多个属性复用。我建议你把序列写成带参数的：

// 参数化序列
sequence s_handshake(signal req, signal ack, int delay);
    @(posedge clk)
    req ##delay ack;
endsequence

// 复用
property p_write;
    @(posedge clk)
    disable iff (rst)
    s_handshake(wr_req, wr_ack, 2);
endproperty

property p_read;
    @(posedge clk)
    disable iff (rst)
    s_handshake(rd_req, rd_ack, 3);
endproperty

这样做的好处很明显——改一个序列，所有用到它的属性自动更新。我在做DDR控制器验证时，光握手序列就写了十几个变体，参数化帮我省了至少一半的代码量。

2.6 小结

今天的内容就这些。总结一下：

序列是描述信号行为的「动词」
属性是给序列加上逻辑条件的「形容词」
断言是最终执行检查的「句子」

你写SVA的时候，就按这个思路来：先想清楚信号怎么变化（序列），再想什么条件下要检查（属性），最后决定是assert还是cover。别一上来就写复杂的嵌套，从最简单的a ##1 b开始，慢慢加条件。

下一章咱们聊聊SVA的时序操作符，我会把##、[*]、[->]这些操作符的细节掰开揉碎了讲。到时候见。

📚 课程目录

2. SVA语法入门：SVA的基本结构、序列与属性的定义

2.1 SVA的基本结构：三层架构

2.2 序列（sequence）的定义

2.3 属性（property）的定义

2.4 完整的断言示例

2.5 序列的复用与参数化

2.6 小结