4. SVA基础语法（二）：序列与属性的实战应用
各位同学，欢迎来到第四讲。上一讲我们聊了SVA的基本结构，今天要深入两个核心概念：序列（sequence）和属性（property）。说白了，这两个东西就是SVA的“左膀右臂”。我个人习惯把序列看作“事件的组合”，把属性看作“对事件的断言”。
4.1 序列（sequence）的定义与使用
先说说序列。什么是序列？序列就是一系列事件的组合。你想想看，验证一个协议，往往不是看单个信号跳变，而是看一组信号在时间上的配合。比如握手协议，先有请求，后有应答，这就是一个序列。
4.1.1 基本序列定义
定义一个序列，用 sequence ... endsequence 包裹起来。看个例子：
sequence req_ack;
@(posedge clk) req ##1 ack;
endsequence这个序列表示：在时钟上升沿，先看到 req 为高，一个时钟周期后，ack 为高。这里的 ##1 就是延迟操作符，表示一个时钟周期。
##1 理解成“延迟1个时间单位”，其实它延迟的是“1个时钟周期”。在同步设计中，这很关键。
4.1.2 带参数的序列
序列也可以带参数，这样复用性更好。比如：
sequence req_ack_delay(cycle);
@(posedge clk) req ##cycle ack;
endsequence调用的时候，你可以指定延迟周期数：
req_ack_delay(2); // 延迟2个周期
req_ack_delay(5); // 延迟5个周期嗯，这里要注意：参数必须是常量，不能是变量。我曾经踩过这个坑，在循环里动态传参，结果编译报错。
4.1.3 序列的复合操作
序列可以组合使用。常用的操作符有：
- and：两个序列都成功
- or：两个序列至少一个成功
- intersect：两个序列同时结束
- within：一个序列在另一个序列内部发生
举个例子：
sequence seq_a;
@(posedge clk) a ##1 b;
endsequence
sequence seq_c;
@(posedge clk) c ##1 d;
endsequence
sequence seq_and;
@(posedge clk) seq_a and seq_c;
endsequence这个 seq_and 表示：a##1b 和 c##1d 这两个序列都要成功。注意，它们可以不同时开始，但都必须完成。
intersect 时犯过错误。它要求两个序列同时开始、同时结束。如果你只是想检查两个序列都发生，用 and 更合适。
4.2 属性（property）的定义与使用
序列是“发生了什么”，属性是“应该发生什么”。属性是断言的灵魂。你定义一个属性，然后用 assert 去检查它。
4.2.1 基本属性定义
属性用 property ... endproperty 定义：
property req_ack_prop;
@(posedge clk) req |-> ##1 ack;
endproperty
assert property (req_ack_prop);这个属性表示：如果 req 为高，那么下一个时钟周期 ack 必须为高。这就是一个典型的蕴含操作。
4.2.2 属性中的蕴含操作符
蕴含操作符是SVA里最常用的。它有两种：
| 操作符 | 含义 | 示例 |
|---|---|---|
|-> |
重叠蕴含（同一周期检查） | a |-> b 表示a为高时，同一周期b必须为高 |
|=> |
非重叠蕴含（下一周期检查） | a |=> b 表示a为高时，下一周期b必须为高 |
我个人习惯这样记：|-> 是“立即检查”，|=> 是“等一个周期再检查”。
看个实际例子：
// 重叠蕴含：写使能时，数据必须有效
property write_data_overlap;
@(posedge clk) write_en |-> data_valid;
endproperty
// 非重叠蕴含：请求后，下一个周期必须有应答
property req_ack_nonoverlap;
@(posedge clk) req |=> ack;
endproperty|->。而请求-应答这种有先后顺序的，用 |=>。选错了，验证结果就全错了。
4.3 序列与属性的配合使用
在实际项目中，序列和属性经常配合使用。我一般这样组织：
- 先定义底层的序列，描述信号的基本时序关系
- 再用属性把这些序列组合起来，形成完整的断言
举个例子：
// 定义序列
sequence s_req;
@(posedge clk) req;
endsequence
sequence s_ack;
@(posedge clk) ##[1:3] ack; // 1到3个周期内应答
endsequence
// 定义属性
property p_req_ack;
@(posedge clk) s_req |-> s_ack;
endproperty
// 断言
assert property (p_req_ack);这个例子中，s_ack 用了 ##[1:3]，表示应答可以在1到3个周期内出现。这种时间窗口在实际验证中非常常见。
4.4 蕴含操作符的深入理解
蕴含操作符看起来简单，但用起来有不少门道。我重点说两个容易混淆的地方。
4.4.1 蕴含的“空成功”问题
你想想看，如果 a |-> b 中，a 从来没有为高过，这个属性算成功还是失败？
答案是：算成功。因为蕴含的语义是“如果a发生，那么b必须发生”。a没发生，条件不成立，自然不算失败。这叫“空成功”（vacuous success）。
我曾经在项目中遇到一个bug：某个信号一直没拉高，导致断言一直空成功，掩盖了真正的设计问题。后来我加了一个覆盖点（cover property）来检查前提条件是否被触发过。
4.4.2 蕴含与序列的嵌套
蕴含操作符后面可以跟复杂的序列：
property complex_prop;
@(posedge clk) a ##1 b |-> c ##1 d;
endproperty这个属性表示：如果看到 a 后一个周期出现 b，那么紧接着 c 后一个周期必须出现 d。说白了，就是“如果前半段序列成功，后半段序列必须成功”。
and、or 等操作，最好加括号明确优先级。我见过有人因为优先级问题，写出来的属性和预期完全不一样。
4.5 实战建议
最后，给各位几个实战建议：
- 从简单开始：先写简单的序列和属性，验证通过后再逐步复杂化
- 多用参数化序列：提高复用性，减少重复代码
- 注意时间窗口：用
##[m:n]而不是固定延迟，更贴近实际协议 - 加覆盖点：检查前提条件是否被触发，避免空成功
好了，这一讲就到这里。序列和属性是SVA的基石，一定要多练。下一讲我们会聊SVA的高级序列操作，包括 throughout、within 等，敬请期待。