3、SVA基础（上）：SVA是什么、SVA的层次结构、序列的基本语法、属性的基本语法
3.1 SVA到底是什么？
说实话，我刚接触形式验证那会儿，对SVA也是一头雾水。总觉得它跟Verilog里的`always`块差不多，不就是写个断言嘛。后来踩了坑才明白——SVA（SystemVerilog Assertions）是一种专门用来描述时序行为的语言。
你可以把它想象成给芯片设计装上一套“监控摄像头”。设计里信号怎么跳变、什么时候该高、什么时候该低，SVA都能精确描述。我习惯把SVA比作“时序警察”——它不参与逻辑运算，只负责盯着信号，一旦违规就报警。
3.2 SVA的层次结构
SVA的层次结构其实很简单，就三层：序列（sequence）→ 属性（property）→ 断言（assert）。我刚开始学的时候总觉得这玩意儿绕，后来自己画了个图才理清楚。
你看，从序列到属性再到断言，是一层一层“包装”上去的。序列是最小的砖块，属性是墙，断言就是质检员。我个人习惯把序列写在最前面，属性在中间，断言放在最后——这样结构清晰，后期维护也方便。
3.3 序列（sequence）的基本语法
序列是SVA的“最小单元”。说白了，它就是描述信号在一段时间内的跳变关系。比如“a信号拉高后，b信号在下一个时钟周期拉高”——这就是一个序列。
3.3.1 最简单的序列
sequence s1;
@(posedge clk) a ##1 b;
endsequence这个序列的意思是：在时钟上升沿，a为高，然后过一个时钟周期，b为高。那个##1就是“延迟一个时钟周期”的意思。我刚开始总把##1理解成“延迟1个时间单位”，后来才发现是“延迟1个时钟周期”——这俩差别可大了。
3.3.2 带延迟范围的序列
sequence s2;
@(posedge clk) a ##[1:3] b;
endsequence这个表示：a拉高后，在1到3个时钟周期内，b必须拉高。我在项目中遇到过这种情况——检查握手信号时，valid拉高后，ready必须在3个周期内响应。用##[1:3]就特别合适。
3.3.3 序列的复合操作
序列还能组合使用。比如“与”操作和“或”操作：
sequence s3;
@(posedge clk) a ##1 b ##1 c;
endsequence
sequence s4;
@(posedge clk) d ##1 e;
endsequence
// 两个序列的“与”
sequence s_and;
@(posedge clk) s3 and s4;
endsequence
// 两个序列的“或”
sequence s_or;
@(posedge clk) s3 or s4;
endsequenceand要求两个序列同时结束，or要求至少一个序列结束。嗯，这里要注意：and和or的起始点必须相同，但结束点可以不同。
and组合两个长度不同的序列，结果仿真一直报错。后来才发现——and要求两个序列同时开始、同时结束。如果长度不同，短的序列会“等待”长的序列结束。
3.4 属性（property）的基本语法
属性比序列多了一层“逻辑包装”。它告诉验证工具：在什么条件下，这个序列应该发生。我习惯把属性理解为“带条件的序列”。
3.4.1 最简单的属性
property p1;
@(posedge clk) disable iff (rst_n)
a ##1 b;
endproperty这个属性表示：在时钟上升沿，如果复位信号rst_n没有拉低，那么a拉高后，下一个周期b必须拉高。disable iff是属性的“开关”——当复位有效时，这个属性被禁用，不检查。
3.4.2 带前提条件的属性
property p2;
@(posedge clk) disable iff (rst_n)
req |=> ##[1:3] gnt;
endproperty这里用到了|=>操作符，意思是“如果req为高，那么接下来...”。这个属性检查的是：当req拉高后，在1到3个周期内，gnt必须拉高。我在项目中用这个检查总线仲裁逻辑，特别好使。
3.4.3 属性的嵌套
属性可以嵌套序列，也可以嵌套其他属性：
property p3;
@(posedge clk) disable iff (rst_n)
s1 and s2;
endproperty
property p4;
@(posedge clk) disable iff (rst_n)
p1 or p2;
endproperty你想想看，这种嵌套能力让SVA的表达力变得非常强。你可以把复杂的时序行为拆成小块，然后像搭积木一样组合起来。
disable iff，再写主体逻辑。因为复位条件是最容易漏掉的——我曾经漏掉复位，结果仿真时复位期间疯狂报错，全是假错。
3.5 序列 vs 属性：到底有什么区别？
这个问题我经常被问到。其实很简单：
| 维度 | 序列（sequence） | 属性（property） |
|---|---|---|
| 核心作用 | 描述信号跳变 | 描述时序约束 |
| 是否带时钟 | 必须带 | 必须带 |
| 是否带复位 | 不带 | 可以带（disable iff） |
| 能否独立使用 | 不能（需要被属性调用） | 可以（配合assert使用） |
| 复用性 | 高（可被多个属性调用） | 中（可被其他属性调用） |
说白了，序列是“素材”，属性是“剧本”。素材可以反复用，剧本决定了最终演什么。我写验证环境时，习惯把通用的序列放在一个包里，属性放在另一个包里——这样维护起来特别方便。
好了，这一章的内容就到这里。SVA的基础语法其实不难，难的是怎么把复杂的时序行为拆解成序列和属性。下一章我们会继续深入SVA的进阶语法，包括蕴含操作符、时序窗口、以及一些高级技巧。
公众号:蓝海资料掘金营，微信deep3321