4. SVA序列与属性：sequence定义、property定义、时钟与复位、蕴含操作符(|->, |=>)、序列匹配
好，咱们今天聊聊SVA里最核心的两个概念——序列和属性。说实话，我刚接触SVA那会儿，总觉得sequence和property长得差不多，用起来也经常搞混。后来踩了几个坑才明白，这俩东西分工其实很明确：sequence管的是信号在时间轴上的行为，property管的是这个行为到底对不对。
4.1 sequence定义——搭积木的基础
sequence说白了就是描述一组信号在时钟沿上的变化规律。你可以把它理解成一段「时间上的模式匹配」。
举个例子，我想描述「a信号拉高后，下一个时钟周期b信号也拉高」这个行为：
sequence seq_ab;
a ##1 b;
endsequence这里的##1表示延迟一个时钟周期。嗯，这里要注意：##0表示同一个时钟周期，##2表示延迟两个周期，以此类推。
我个人习惯把sequence写得尽量短小精悍，方便复用。比如：
sequence req_ack;
req ##[1:3] ack; // req拉高后，1到3个周期内ack必须拉高
endsequence我在项目中遇到过这样一个坑：有人把##[1:3]写成了##[1:3]，结果仿真跑了一整天才发现——其实语法没错，但时序范围搞错了，导致验证漏掉了一个边界情况。所以，延迟范围一定要和设计规格对清楚。
4.2 property定义——把序列变成断言
sequence只是描述了行为，但property才真正告诉工具「这个行为应该总是成立」或者「这个行为应该永不发生」。
看个例子：
property p_req_ack;
@(posedge clk) req |=> ack;
endproperty这里@(posedge clk)指定了时钟，|=>是蕴含操作符。整个property的意思是：在每个时钟上升沿，如果req为高，那么下一个时钟周期ack必须为高。
你可能会问：那直接用sequence不行吗？其实sequence只是描述了「如果req高，然后ack高」这个模式，但property才规定了「每次req高，后面都必须跟ack高」——多了个「每次」和「必须」，这就是本质区别。
核心区别一句话：sequence描述「发生了什么」，property描述「应该发生什么」。
4.3 时钟与复位——SVA的命脉
SVA里时钟是灵魂。没有时钟，序列和属性就不知道在哪个时间点去采样信号。
时钟定义有两种常见写法：
// 写法一：在property里指定
property p_example;
@(posedge clk) a ##1 b;
endproperty
// 写法二：在sequence里指定（不推荐，容易乱）
sequence s_example;
@(posedge clk) a ##1 b;
endsequence我个人强烈建议只在property层面写时钟，sequence里不要写。为什么？因为一旦sequence里写了时钟，复用时时钟就绑死了，灵活性大打折扣。我曾经接手过一个项目，里面sequence到处都嵌了时钟，想换个时钟域验证，结果改得我头皮发麻。
复位呢？SVA里复位通常用disable iff来处理：
property p_example_with_reset;
@(posedge clk) disable iff (rst_n) a ##1 b;
endproperty这个disable iff (rst_n)的意思是：如果复位信号rst_n为低（有效），就禁用这个属性的检查。注意，复位信号一般用低电平有效，这是业界惯例。
避坑指南：我曾经见过有人把disable iff写成了if (!rst_n) disable，语法上没错，但语义完全不同。disable iff是立即终止当前正在进行的序列匹配，而if语句只是条件判断。这两者在时序上的表现天差地别。
4.4 蕴含操作符(|->, |=>)——SVA的灵魂
蕴含操作符是SVA里最强大的工具，没有之一。它表达了「如果...那么...」的逻辑关系。
两种蕴含操作符：
| 操作符 | 含义 | 示例 | 说明 |
|---|---|---|---|
|-> |
立即蕴含 | a |-> b |
如果a在当前周期为高，那么b必须在同一个周期为高 |
|=> |
非立即蕴含 | a |=> b |
如果a在当前周期为高，那么b必须在下一个周期为高 |
你想想看，这两个操作符的区别其实就是「一个时钟周期的延迟」。但实际用起来，很多人会搞混。我有个小技巧：看到|->就想到「同时」，看到|=> 就想到「下一拍」。
来个复杂点的例子：
property p_pipeline;
@(posedge clk) disable iff (rst_n)
(req & grant) |=> ##2 data_valid;
endproperty这个property的意思是：如果req和grant同时为高，那么两个周期后data_valid必须为高。注意，|=> 后面跟了##2，表示在下一个周期的基础上再延迟两个周期——也就是总共延迟三个周期。
个人经验：写蕴含操作符时，我建议先把「前提条件」和「结论」分开想清楚。前提写在|->或|=> 左边，结论写在右边。如果结论需要多个周期才能完成，就用##或者序列来扩展。
4.5 序列匹配——验证的最后一公里
序列匹配，说白了就是检查信号序列是否和预期一致。SVA提供了多种匹配方式：
- 精确匹配：
a ##1 b ##1 c，要求a、b、c严格按顺序出现 - 范围匹配：
a ##[1:3] b，b可以在a之后的1到3个周期内出现 - 重复匹配：
a ##1 b[*3]，b连续出现3个周期 - 非连续重复：
a ##1 b[=2]，b总共出现2次，不要求连续 - 跟随匹配：
a ##1 b[->2]，b出现第2次时匹配成功
举个例子，我想验证「请求发出后，响应必须在3到5个周期内回来」：
sequence s_req_resp;
req ##[3:5] resp;
endsequence
property p_req_resp;
@(posedge clk) disable iff (rst_n)
req |-> s_req_resp;
endproperty这里##[3:5]就是范围匹配，resp可以在req之后的第3、4或5个周期出现，都算匹配成功。
我在项目中遇到过这样一个场景：某个接口协议要求ack信号在req拉高后的2到4个周期内拉高，但设计人员写成了固定3个周期。我们用##[2:4]去验证，结果仿真通过了——因为3在2到4之间。但后来发现，如果设计改成2个周期，验证环境照样能过，但协议其实要求的是「至少2个周期，最多4个周期」。所以，范围匹配虽然灵活，但一定要确认你的范围是否真的反映了设计需求。
知识体系总览
下面这张图帮你理清本章的核心脉络：
这张图把sequence和property的关系、各自的子功能以及最终的应用串在了一起。你可以看到，sequence负责描述信号的时间行为，property负责加上时钟、复位和逻辑约束，最后通过assert property变成真正的断言检查。
好了，关于SVA序列与属性的核心内容就这些。记住：sequence是砖，property是墙，蕴含操作符是水泥。把这三样东西玩转了，SVA你就掌握了八成。
一句话总结：sequence定义行为模式，property定义检查规则，时钟和复位是运行环境，蕴含操作符是逻辑骨架，序列匹配是最终检验手段。
可可精品资料库