2. SVA语法入门：立即断言与并发断言，sequence与property基础
好，咱们正式开始啃SVA这块硬骨头。说实话，很多工程师一看到断言就头大，觉得语法太绕。我刚开始接触SVA时也差不多，总觉得这东西不就是写几个检查条件吗？怎么搞得这么复杂。但后来在项目里吃过亏——有一次仿真跑了两周，结果发现一个地址对齐的bug，要是早点用断言，半天就能揪出来。从那以后，我就老老实实学SVA了。
今天咱们先搞定两个最基础的概念：立即断言和并发断言，以及它们的核心搭档——sequence和property。说白了，这是SVA的“动词”和“名词”，搞懂它们，你就能写出80%的常用断言。
2.1 立即断言：简单粗暴的“现场检查”
立即断言，英文叫Immediate Assertion。它的特点就一个字：快。在仿真执行的当前时刻，立刻检查条件是否成立。如果条件不满足，立马报错。
语法很简单：
label: assert (expression) else $error("消息");举个例子：
always_ff @(posedge clk) begin
if (valid) begin
check_data: assert (data != 0) else $error("valid时data不能为0");
end
end嗯，这里要注意：立即断言是过程性代码，必须写在always块、initial块或者function/task里。它不像并发断言那样可以独立存在。
我的个人习惯：在组合逻辑或简单的时序检查中，我更喜欢用立即断言。比如检查状态机是否进入非法状态、FIFO是否溢出。这些场景下，立即断言写起来快，读起来也直观。
我曾经踩过的坑：立即断言在时钟沿触发时，如果表达式里用了非阻塞赋值（<=），可能会检查到旧值。我曾经在检查握手协议时，valid和ready的时序差了一个周期，断言死活不报错，后来才发现是赋值方式的问题。所以，立即断言里尽量用阻塞赋值（=）或者直接用组合逻辑。
2.2 并发断言：时序世界的“监控探头”
并发断言（Concurrent Assertion）才是SVA的精髓。它不关心你在哪个always块里，它只关心时序关系。你想想看，一个信号拉高后，另一个信号必须在3个周期内拉高——这种跨周期的检查，立即断言就搞不定了。
并发断言的基本格式：
label: assert property (property_expr) else $error("消息");注意这个property关键字，它是并发断言的核心。property里可以写各种时序表达式，比如：
property p_req_ack;
@(posedge clk) req |=> ##[1:3] ack;
endproperty
a_req_ack: assert property (p_req_ack) else $error("req后1~3周期内ack未拉高");这个断言的意思是：在时钟上升沿，如果req为高，那么接下来的1到3个周期内，ack必须至少拉高一次。你看，这就是并发断言的力量——它描述的是跨周期的行为。
核心区别一句话总结：
- 立即断言：检查“当前时刻”的条件，写在过程块里
- 并发断言：检查“跨周期”的时序关系，写在property里，独立于过程块
2.3 sequence：时序的“基本单元”
sequence是SVA里最常用的“积木”。你可以把它理解成一组信号的时序模式。比如“req拉高后，在下一个时钟沿gnt拉高”，这就是一个sequence。
定义sequence的语法：
sequence name;
signal_expr ## delay signal_expr ...;
endsequence常用的操作符：
| 操作符 | 含义 | 示例 |
|---|---|---|
| ##n | 延迟n个时钟周期 | a ##2 b 表示a拉高后2个周期b拉高 |
| ##[m:n] | 延迟m到n个周期 | a ##[1:3] b 表示a后1~3周期内b拉高 |
| and | 两个序列同时结束 | seq1 and seq2 |
| or | 两个序列任一结束 | seq1 or seq2 |
| intersect | 两个序列长度相等且同时结束 | seq1 intersect seq2 |
举个例子：
sequence s_req_gnt;
req ##[1:3] gnt;
endsequence
sequence s_data_valid;
data_valid ##0 data_ready;
endsequence我个人习惯把sequence当作“函数”来用——把常用的时序模式封装起来，然后在property里调用。这样property读起来就像自然语言一样清晰。
2.4 property：断言的“完整句子”
如果说sequence是“名词短语”，那property就是“完整句子”。property里可以包含sequence，也可以加上一些逻辑条件，比如“只有在reset无效时才检查”。
property的基本结构：
property name;
@(时钟边沿) 使能条件 |-> 时序表达式;
endproperty这里有两个关键操作符：
- |->：重叠蕴含。左边条件成立时，当前时刻右边必须成立。
- |=> ：非重叠蕴含。左边条件成立时，下一个时钟沿右边必须成立。
看个实际例子：
property p_write_strobe;
@(posedge clk)
disable iff (rst_n == 0) // 复位时不检查
write_en |-> strobe == 1; // write_en拉高时，strobe必须为高
endproperty
a_write_strobe: assert property (p_write_strobe)
else $error("write_en时strobe未拉高");你发现没有？property把“什么时候检查”、“什么条件下检查”、“检查什么时序”这三件事分得清清楚楚。这就是SVA的设计哲学——关注点分离。
我建议：刚开始写SVA时，先别急着写复杂的property。先从简单的sequence开始，比如“req后跟ack”、“valid后跟ready”。等sequence写顺了，再把它组合到property里。就像搭积木，先搭小件，再拼大件。
2.5 知识体系总览
下面这张图是我自己整理的SVA基础结构，你看一眼就能明白它们之间的关系：
从这张图你能看到：assert property在最顶层，它调用property；property里包含sequence（描述时序）和disable iff（描述例外条件）；sequence底层由各种时序操作符组成。一层套一层，结构非常清晰。
2.6 实战建议：从哪开始写？
说了这么多，你可能还是有点懵——到底该先写sequence还是先写property？
我的做法是：
- 先找接口协议的关键时序。比如握手协议里的valid/ready、总线协议里的地址/数据/控制信号。
- 把每个时序关系写成独立的sequence。比如“valid拉高后ready必须在3周期内拉高”，写成
valid ##[0:3] ready。 - 把sequence组合到property里，加上使能条件和复位屏蔽。
- 最后用assert property启动检查。
举个例子，假设你要检查AXI协议的写地址通道：
// 第1步：定义sequence
sequence s_awvalid_awready;
awvalid ##[0:3] awready;
endsequence
// 第2步：定义property
property p_aw_channel;
@(posedge aclk)
disable iff (aresetn == 0)
s_awvalid_awready;
endproperty
// 第3步：启动断言
a_aw_channel: assert property (p_aw_channel)
else $error("AW通道握手超时");你看，三步走下来，一个完整的断言就写好了。是不是比想象中简单？
我曾经犯过的错：刚开始写SVA时，我总想把所有检查写在一个超级长的property里。结果仿真报错时，根本分不清是哪个时序出了问题。后来我学乖了——一个property只检查一件事。宁可多写几个断言，也别堆在一起。这样调试时，看报错消息就能直接定位问题。
好了，这一章的内容就到这儿。立即断言和并发断言的区别、sequence和property的用法，这些都是SVA的基石。下一章咱们会深入讲sequence的更多操作符，以及如何在property里使用形式参数——说白了就是让断言变得更灵活、更可复用。到时候我会拿一个实际项目中的总线协议来做例子，保证你听完就能上手写。
可可精品资料库