3. SVA序列(sequence)：基本序列、序列操作符、序列匹配

各位同学，咱们今天聊聊SVA里最核心的东西——序列（sequence）。

说实话，我刚接触SystemVerilog Assertion那会儿，觉得序列这玩意儿挺玄乎的。后来做项目做多了才发现，它其实就是把一堆信号的变化规律给描述出来。你想想看，验证的本质不就是检查信号是不是按我们期望的方式变化吗？

3.1 什么是序列？

序列，说白了就是一组布尔表达式在时间上的组合。它描述的是信号从一种状态到另一种状态的演变过程。

举个例子：

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

这个序列表示：a为真，然后过一个时钟周期b为真，再过两个时钟周期c为真。就这么简单。

我在项目中遇到过很多新人，一上来就写复杂的断言，结果仿真跑不通。我建议你从最基本的序列开始，一步一步来。

3.2 基本序列

基本序列有三种形式：

类型	写法	含义
单周期序列	a	当前时钟周期a为真
多周期序列	a ##1 b	a为真，下一周期b为真
连续序列	a ##0 b	a和b在同一周期为真

嗯，这里要注意：##0表示同一个时钟周期，##1表示下一个时钟周期。千万别搞混了。

3.3 序列操作符

序列操作符是SVA的精华所在。我刚开始学的时候，觉得这些操作符特别多，记不住。后来发现，常用的就那么几个。

3.3.1 延迟操作符 ##

这个最常用。它指定了两个事件之间的时钟周期数。

// 延迟1个周期
a ##1 b

// 延迟3个周期
a ##3 b

// 延迟范围
a ##[1:3] b  // 1到3个周期后b为真

我曾经在调试一个DDR控制器的时候，发现时序总对不上。后来用##[1:5]这种范围延迟，一下子就定位到了问题。说白了，范围延迟给了你一定的容错空间。

3.3.2 重复操作符

重复操作符有三种：

• 连续重复：a[*3] — a连续为真3个周期
• 非连续重复：a[=3] — a为真3次，但不要求连续
• 跟随重复：a[->3] — a为真3次，且最后一次触发后续序列

举个例子：

// 连续重复：请求信号连续拉高3个周期
sequence req_hold;
    req[*3];
endsequence

// 非连续重复：中断信号出现3次
sequence int_occur;
    int[=3];
endsequence

我个人习惯用连续重复比较多，因为它直观。非连续重复和跟随重复，说实话，用得少一些，但在某些场景下确实很管用。

3.3.3 逻辑操作符

序列也支持逻辑操作：

• and：两个序列都匹配
• or：任一序列匹配
• intersect：两个序列同时结束

sequence s_and;
    (a ##1 b) and (c ##2 d);
endsequence

sequence s_or;
    (a ##1 b) or (c ##2 d);
endsequence

sequence s_intersect;
    (a ##1 b) intersect (c ##2 d);
endsequence

这里有个坑，我踩过。intersect要求两个序列的结束时间必须完全一致。如果长度不一样，它永远不会匹配。你想想看，这多坑人？

3.4 序列匹配

序列匹配，就是检查序列是否按照预期发生了。SVA提供了两种匹配方式：

3.4.1 立即断言

always @(posedge clk) begin
    if (a && b)
        $display("匹配成功");
end

这种写法简单，但不够灵活。我一般只在调试的时候用。

3.4.2 并发断言

property p1;
    @(posedge clk) a ##1 b;
endproperty

assert property (p1);

并发断言才是SVA的精髓。它会在每个时钟周期自动检查，而且支持复杂的时序关系。

3.5 实战经验分享

我在做某个AI芯片项目时，需要验证一个复杂的握手协议。协议要求：请求信号拉高后，应答信号必须在3到5个周期内拉高，且应答拉高后请求必须立即拉低。

用序列来描述就是：

sequence handshake;
    req ##[3:5] ack ##0 !req;
endsequence

property p_handshake;
    @(posedge clk) $rose(req) |-> handshake;
endproperty

assert property (p_handshake);

你看，用序列描述这种时序关系，多清晰！

3.6 知识体系总览

下面这张图，是我自己整理的序列知识体系。你把它理解了，序列这块就差不多了。

这张图把序列分成了三大块：基本序列、序列操作符、序列匹配。你把这三大块搞明白了，写SVA就跟玩似的。

好了，序列这块就讲这么多。记住，多写多练，自然就熟了。我刚开始也是从最简单的a ##1 b开始写的，慢慢就上手了。