4. 序列与属性：序列定义与操作符、属性定义与操作符、蕴含操作符

各位好，这一节我们聊聊SVA（SystemVerilog Assertion）里最核心的两个概念——序列和属性。

说实话，我刚学SVA那会儿，经常搞混sequence和property。后来踩了几个坑才明白：序列是描述信号怎么跳变的，属性是描述这些跳变应该满足什么条件。说白了，序列是“发生了什么”，属性是“这应该是对的”。

4.1 序列定义与操作符

序列，就是一组按时间顺序排列的事件。我们用sequence来定义它。

4.1.1 基本序列定义

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

// 带延迟的序列：a为高，1个时钟后b为高
sequence s_a_then_b;
    @(posedge clk) a ##1 b;
endsequence

这里##1表示延迟一个时钟周期。我个人习惯把这种延迟叫做“拍”，一拍就是一次时钟沿。

4.1.2 序列操作符

序列操作符是SVA的“语法糖”，用好了能写出很优雅的断言。我整理了一张表，方便大家查阅：

操作符	含义	示例	说明
##n	固定延迟n个时钟	a ##2 b	a为高后，正好2拍后b为高
##[m:n]	延迟范围m到n个时钟	a ##[1:3] b	a为高后，1到3拍内b为高
[*n]	重复n次	a[*3]	a连续3拍为高
[*m:n]	重复m到n次	a[*2:4]	a连续2到4拍为高
[->n]	非连续重复（goto）	a[->2]	a出现第2次为高（中间可间隔）
[=n]	非连续重复（non-consecutive）	a[=2]	a出现第2次为高，且之后a为低
and	两个序列同时结束	s1 and s2	s1和s2都在同一拍结束
or	两个序列任一结束	s1 or s2	s1或s2中先结束的那个
intersect	两个序列长度相同且同时结束	s1 intersect s2	比and更严格，长度必须相等
within	一个序列包含在另一个序列内	s1 within s2	s1的起止时间在s2的起止时间内

4.1.3 序列操作符实战

来看一个实际例子。我在做DDR控制器验证时，需要检查读命令后数据返回的时序：

// 读命令发出后，2到5拍内数据有效
sequence read_data_valid;
    @(posedge clk) 
        read_cmd ##[2:5] data_valid;
endsequence

// 连续3次握手成功
sequence three_handshakes;
    @(posedge clk) 
        handshake[*3];
endsequence

// 请求与应答同时结束
sequence req_ack_sync;
    @(posedge clk) 
        request and acknowledge;
endsequence

嗯，这里要注意and和intersect的区别。我曾经在项目中用and检查两个握手信号，结果漏掉了一个bug——两个信号长度不一样，但and只关心结束点，不关心长度。后来改成intersect才抓住问题。

4.2 属性定义与操作符

属性是序列的“升级版”。序列只描述事件，属性则描述这些事件应该满足什么条件。属性里可以放序列，也可以放更复杂的逻辑。

4.2.1 属性定义

// 一个简单的属性：a为高后，b最终必须为高
property p_a_then_b;
    @(posedge clk) 
        a |-> ##[1:5] b;
endproperty

// 带使能条件的属性
property p_enabled_req;
    @(posedge clk) 
        disable iff (!rst_n)
        enable |-> req ##1 ack;
endproperty

disable iff是个好东西。它让属性在复位时自动失效，不会报假错。我刚开始写断言时经常忘记加这个，结果仿真一复位就报一堆错，后来就养成习惯了——所有属性都加上disable iff。

4.2.2 属性操作符

属性操作符比序列操作符少一些，但每个都很关键：

操作符	含义	示例	说明
|->	蕴含（overlap）	a |-> b	a为高时，同一拍b必须为高
|=>	蕴含（non-overlap）	a |=> b	a为高时，下一拍b必须为高
not	取反	not (a ##1 b)	序列不成立
always	始终成立	always (a |-> b)	每个时钟沿都检查
s_eventually	最终成立	s_eventually a	未来某个时刻a会为高

4.3 蕴含操作符：overlap vs non-overlap

蕴含操作符是SVA里最常用、也最容易搞混的东西。说白了，它就是个“如果...那么...”的逻辑。

4.3.1 Overlap蕴含（|->）

这个操作符的意思是：如果左边条件成立，在同一时钟周期右边也必须成立。

// 例子：当valid为高时，同一拍data必须有效
property p_valid_data_overlap;
    @(posedge clk) 
        valid |-> data_valid;
endproperty

// 更复杂的：valid为高时，同一拍开始一个序列
property p_valid_seq_overlap;
    @(posedge clk) 
        valid |-> (req ##1 ack ##1 grant);
endproperty

我在项目中遇到过这样一个场景：总线协议要求地址和数据在同一拍有效。用|->就对了，因为地址和数据是同时发出的。

4.3.2 Non-overlap蕴含（|=>）

这个操作符的意思是：如果左边条件成立，下一个时钟周期右边必须成立。

// 例子：当req为高时，下一拍ack必须为高
property p_req_ack_nonoverlap;
    @(posedge clk) 
        req |=> ack;
endproperty

// 带延迟的：req为高后，2到4拍内ack必须为高
property p_req_ack_delayed;
    @(posedge clk) 
        req |=> ##[2:4] ack;
endproperty

4.3.3 蕴含操作符的嵌套

实际项目中，我们经常需要嵌套使用蕴含操作符。来看一个复杂点的例子：

// 当使能信号为高时，检查握手协议
property p_handshake_with_enable;
    @(posedge clk) 
        disable iff (!rst_n)
        enable |-> (req |=> ack ##1 grant);
endproperty

// 更复杂的：检查总线事务
property p_bus_transaction;
    @(posedge clk) 
        disable iff (!rst_n)
        // 当总线空闲时，发起传输
        (bus_idle |-> (req ##[1:3] ack))
        // 并且传输完成后，总线必须回到空闲
        and
        (ack |=> ##1 bus_idle);
endproperty

你看，属性可以组合多个蕴含操作符，形成复杂的时序检查。这就是SVA的强大之处。

4.4 知识体系总览

为了让大家更直观地理解序列和属性的关系，我画了一张图：

4.5 实战建议

最后，分享几个我在项目中总结的经验：

• 先写序列，再写属性：我习惯先把信号间的时序关系写成序列，然后再用属性把它们“包装”起来。这样思路清晰，不容易出错。
• 多用disable iff：每个属性都加上复位条件，避免仿真初期报一堆假错。
• 区分overlap和non-overlap：写蕴含操作符前，先问自己“这个协议是同一拍还是下一拍？”想清楚了再下笔。
• 复杂属性拆开写：如果一个属性太长，拆成多个小属性。调试时能快速定位问题。

好了，序列和属性这部分就聊到这儿。记住一句话：序列是砖，属性是墙，蕴含操作符是水泥。把这三样东西用好，你的断言就能既坚固又优雅。