2. SVA语法入门：SVA的基本结构，序列(sequence)与属性(property)的概念

好，咱们正式开始啃SVA这块硬骨头。说实话，我刚开始学SVA的时候，觉得这东西不就是写几个断言嘛，能有多难？结果第一次写就把自己坑了——一个简单的握手协议断言，仿真跑了三天才发现写反了时序关系。嗯，从那以后我老老实实把基础打扎实了。

今天咱们就聊聊SVA最核心的两个概念：序列(sequence)和属性(property)。说白了，这两个东西就是SVA的"主语"和"谓语"。

先看一个最简单的SVA断言长什么样：

assert property (@(posedge clk) a |-> b);

这行代码的意思是：在每个时钟上升沿，如果a为真，那么b也必须为真。就这么简单。

但实际项目中，我们很少写这么简单的断言。我个人的习惯是，先把SVA的结构拆成三块：

你想想看，这就像写一个"如果...那么..."的句子。序列就是"如果"部分，属性就是"那么"部分，断言就是句号。

核心要点：SVA断言 = 序列 + 属性 + 断言关键字。三者缺一不可。

序列是什么？说白了就是信号在时钟边沿上的变化模式。比如"a信号拉高后，两个时钟周期内b信号必须拉低"——这就是一个序列。

看个例子：

sequence s_req_ack;
    @(posedge clk) req ##2 ack;
endsequence

这个序列描述的是：在时钟上升沿看到req为高，然后过2个时钟周期，ack必须为高。##2就是"延迟2个时钟周期"的意思。

我在项目中遇到过一种情况：有人把##2理解成"延迟2个时间单位"，结果仿真结果完全不对。记住，在SVA里，##n默认是延迟n个时钟周期，不是时间单位。

序列还可以组合：

sequence s_req_ack_or;
    @(posedge clk) (req ##2 ack) or (req ##3 ack);
endsequence

这个序列表示：req拉高后，要么2个周期后ack拉高，要么3个周期后ack拉高。两种都算匹配。

小技巧：写序列时，我习惯先画个时序图，把信号的变化点标出来。这样写出来的序列基本不会错。

属性是序列的"升级版"。它给序列加上了触发条件和逻辑关系。

看个例子：

property p_req_ack;
    @(posedge clk) req |-> ##2 ack;
endproperty

这个属性说的是：如果req为高，那么2个周期后ack必须为高。|->是"蕴含"操作符，左边是条件，右边是结果。

你可能会问：这和序列有什么区别？

区别大了。序列只是描述"发生了什么事"，属性描述的是"如果发生了A，那么应该发生B"。属性有因果关系，序列没有。

我再给你看个更复杂的属性：

property p_req_ack_no_overlap;
    @(posedge clk) $rose(req) |-> ##[1:3] ack ##1 !ack;
endproperty

这个属性说的是：当req从0变1时，在接下来的1到3个周期内ack必须拉高，然后下一个周期ack必须拉低。这就是一个典型的"请求-应答-释放"协议。

注意：我曾经犯过一个错误——把|->和|=>搞混了。|->是"立即蕴含"，|=>是"非重叠蕴含"。前者要求结果在同一个时钟周期发生，后者要求结果在下一个时钟周期发生。用错了，断言就废了。

我画了一张图，帮你理清序列和属性的关系：

从这张图你可以看到：序列是"原材料"，属性是"半成品"，断言是"成品"。序列描述信号怎么变，属性描述规则是什么，断言告诉工具去检查。

我整理了几个项目中常用的序列和属性模式，你直接拿去用：

避坑指南：我曾经在项目里用##[1:$]写了一个"等待中断"的序列，结果仿真跑了三天没结束。为什么？因为$表示无限等待，如果中断一直不来，仿真就卡死了。后来我改成##[1:100]，加了个超时限制，问题就解决了。

最后说个细节——命名。我见过太多人给序列和属性起名叫seq1、prop2，调试的时候根本分不清哪个是哪个。

我个人习惯：

这样一眼就能看出代码里哪些是序列、哪些是属性、哪些是断言。调试的时候特别方便。

好了，今天的内容就到这里。序列和属性是SVA的基石，你把这俩搞明白了，后面学操作符、学断言控制，都会轻松很多。