3. SVA序列与属性：sequence、property的构建与层次化

各位同学，今天我们来聊聊SVA里最核心的两个概念——sequence和property。说实话，我刚接触SystemVerilog Assertion那会儿，也被这两个东西绕得晕头转向。后来做项目做多了，才慢慢摸清楚它们的脾气。

简单来说，sequence描述的是信号在时间轴上的行为模式，而property则是在sequence的基础上加上逻辑判断和时序约束。你可以把sequence想象成“发生了什么”，property则是“这个发生应该满足什么条件”。

3.1 sequence：时间上的“故事线”

sequence说白了就是一组信号在时钟节拍上的变化序列。我习惯把它叫做“时间线上的故事”。

sequence  sequence_name;
  信号表达式  [时序操作符]  信号表达式  ...;
endsequence

举个例子，假设我们要描述“a信号拉高后，下一个时钟周期b信号也拉高”：

sequence seq_a_then_b;
  @(posedge clk) a ##1 b;
endsequence

这里的##1就是延迟一个时钟周期。我在项目中遇到过不少新手把##0和##1搞混——##0表示同一个时钟周期内，##1才是下一个时钟周期。嗯，这个坑我踩过。

3.2 property：给sequence加上“规矩”

sequence只管描述行为，但property要告诉验证环境：这个行为是必须发生的，还是禁止发生的。

property property_name;
  时序域  [disable iff(条件)]  断言操作符  sequence;
endproperty

我个人习惯把property分成三类：

• assert property：必须成立，否则报错
• assume property：假设成立，用于约束激励
• cover property：覆盖监控，看看这个场景有没有跑到

你想想看，如果只写sequence不写property，那就像你画了一张地图但没告诉别人该往哪走——没什么用。

3.3 层次化构建：从小sequence搭出大property

实际项目中，我们不会把所有的逻辑都塞进一个sequence里。那样太乱了，也不好维护。我建议的做法是：先定义小的原子sequence，再组合成复杂的property。

举个例子，我们要验证“请求信号req拉高后，最多3个周期内必须收到应答ack”：

// 原子sequence：请求发生
sequence req_asserted;
  @(posedge clk) $rose(req);
endsequence

// 原子sequence：应答收到
sequence ack_received;
  @(posedge clk) $rose(ack);
endsequence

// 组合property：req后最多3拍内ack
property req_ack_max3;
  @(posedge clk) 
  req_asserted |-> ##[1:3] ack_received;
endproperty

assert property (req_ack_max3);

这样做的好处是什么？复用性强。我在一个PCIe项目中，把几十个原子sequence像搭积木一样组合，最后只用了不到200行代码就覆盖了上千条协议规则。要是全写在一起，那代码量至少翻三倍。

3.4 时序操作符：控制时间的“魔法棒”

SVA里最常用的时序操作符，我整理了一张表：

3.5 disable iff：优雅地处理复位

做验证的都知道，复位期间断言不能乱报。这时候disable iff就派上用场了。

property p_req_ack;
  @(posedge clk) disable iff (rst_n == 1'b0)
  req |-> ##[1:3] ack;
endproperty

我曾经见过有人不用disable iff，而是在每个sequence里手动判断复位信号。结果代码又臭又长，还容易漏掉某些路径。记住：能用语言特性解决的问题，别自己造轮子。

3.6 实战中的层次化设计思路

最后，我分享一下在项目中总结的层次化设计流程：

1. 拆解协议规则：把复杂的协议拆成最小的原子行为
2. 编写原子sequence：每个sequence只描述一个简单行为
3. 组合成property：用逻辑操作符和时序操作符把sequence串起来
4. 绑定到模块：用bind语句把property挂到DUT上

好了，关于sequence和property的构建与层次化，今天就聊到这里。记住：好的SVA代码，读起来应该像一篇清晰的文档，而不是一团乱麻。