2. SVA语法入门：SVA的基本结构、序列与属性

好，咱们今天聊聊SVA的语法入门。说实话，很多工程师一看到SVA就觉得头大——又是序列又是属性的，感觉像在学一门新语言。但你别怕，SVA的核心其实就两个东西：序列（sequence）和属性（property）。搞懂了这俩，你就掌握了SVA的半壁江山。

SVA断言长什么样？我直接给你看个最简单的例子：

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

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

一个完整的SVA断言，通常包含三个部分：

核心要点：SVA断言 = 断言关键字 + 属性 + 时钟事件。记住这个公式，后面所有复杂的东西都是在这个基础上堆叠的。

我个人习惯把SVA断言分成两类：

小提示：我在项目中几乎只用并发断言。立即断言调试起来太痛苦了，你想想看，一个信号变化了，断言立刻触发，你根本不知道它是在哪个时钟周期出的问题。

序列是什么？说白了，序列就是描述信号在一段时间内的行为模式。它是SVA最基本的时序单元。

看个例子：

sequence s1;
  a ##1 b ##2 c;
endsequence

这个序列s1描述了什么？

注意这里的##符号，它是SVA里表示延迟的运算符。##n表示延迟n个时钟周期。

避坑指南：我曾经在项目里犯过一个低级错误——把##1理解成延迟1个周期，结果发现它其实是延迟恰好1个周期。如果你想要"0到1个周期"的延迟，得用##[0:1]。这个坑我踩过，你别再踩了。

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

为什么会需要这些操作符？你想想看，实际项目中的时序关系哪有那么简单。比如我要检查"请求发出后，1到3个周期内必须收到响应"，用##[1:3]就搞定了。

序列只是描述了信号的行为，而属性则是在序列的基础上加上逻辑判断。属性才是断言的灵魂。

看个完整的例子：

property p1;
  @(posedge clk) req |-> ##[1:3] ack;
endproperty

assert property (p1);

这个属性p1的意思是：在时钟上升沿，如果req为真，那么接下来1到3个周期内，ack必须为真。

属性里最常用的就是蕴含操作符：

关键区别：|->和|=>就差一个周期。我刚开始学的时候也搞混过，后来记住一句话就再也没错过——"箭头带等号，多等一拍"。

属性还可以嵌套：

property p2;
  @(posedge clk) 
    disable iff (rst)  // 复位时禁用断言
    req |-> ##1 ack ##1 data_valid;
endproperty

这里用到了disable iff，意思是当rst为真时，这个属性不检查。这个在实际项目中太常用了——复位期间信号乱跳，你总不能让它报一堆假错吧？

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

从这张图你可以看到：序列是基础，属性是在序列上加了逻辑条件，而断言则是把属性真正用起来。三者层层递进。

最后分享几个我在项目中积累的经验：

序列命名要规范：我习惯用s_前缀表示序列，p_前缀表示属性。比如s_req_ack、p_req_ack_check。这样看代码一目了然。
复杂序列拆着写：别试图在一个序列里写完所有逻辑。拆成多个小序列，再用and/or组合，调试起来方便得多。
多用cover属性：很多人只写assert，不写cover。但cover能告诉你"这个场景到底有没有被触发过"。我在调试死锁问题时，就是靠cover发现某个状态根本没进入过。
时钟一定要写对：这个听起来是废话，但我真见过有人把posedge写成negedge，然后查了一下午的bug。

个人经验：刚开始写SVA时，建议先画时序图，把信号的变化画清楚，再转成序列和属性。我到现在遇到复杂协议时，还是会先在纸上画时序图。别嫌麻烦，这步省不了。

嗯，SVA的基本结构、序列和属性就讲到这里。这些东西看着简单，但用好了能解决大问题。下一节咱们聊聊SVA的进阶语法——到时候我会分享一个我踩过的深坑，保证让你印象深刻。

可可精品资料库