3. SVA语法入门：SVA的基本结构、序列与属性、断言的关键字

好，咱们进入SVA的实战环节了。说实话，很多工程师一看到SVA的语法就头大，觉得又是序列又是属性的，绕来绕去。我刚开始学的时候也这样，总觉得这东西不就是写个检查条件吗？干嘛搞得这么复杂？

后来在项目里吃过亏才明白——SVA的语法设计，其实是为了让你精确描述时序行为。你想想看，一个信号在时钟上升沿拉高，三个周期后另一个信号必须拉低——这种话用自然语言说清楚都费劲，更别说让工具自动检查了。

3.1 SVA的基本结构

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

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

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

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

• 断言关键字：assert、assume、cover，告诉工具你要干嘛
• 属性(property)：描述你要检查的时序行为
• 序列(sequence)：描述信号在时间上的变化模式

我个人习惯把SVA断言想象成"带时间轴的if-then语句"。普通的if-then只检查当前时刻，SVA可以检查未来几个周期的事情。

3.2 序列(sequence)——描述信号的时间模式

序列是SVA的基础构件。它描述的是：在一段时间内，信号如何变化。

最简单的序列就是单个信号：

sequence s1;
  a && b;  // 同一时刻a和b都为高
endsequence

稍微复杂一点，带时序的：

sequence s2;
  a ##1 b;  // a为高，下一个周期b为高
endsequence

这里的##1就是"延迟一个时钟周期"的意思。我在项目中遇到过有人把##1和##0搞混——##0表示同一个周期，##1表示下一个周期，这个区别很重要。

常用的序列操作符：

操作符	含义	示例
##n	延迟n个时钟周期	a ##2 b (a之后2周期b为高)
##[m:n]	延迟范围，m到n个周期	a ##[1:3] b (a之后1~3周期内b为高)
and	两个序列同时结束	s1 and s2
or	两个序列任一结束	s1 or s2
intersect	两个序列同时开始且同时结束	s1 intersect s2
within	一个序列包含在另一个序列内	s1 within s2

3.3 属性(property)——定义检查规则

属性是SVA的灵魂。它把序列组合起来，加上逻辑条件，形成完整的检查规则。

最常见的属性结构是蕴含操作：

property p1;
  @(posedge clk) a |-> ##1 b;
endproperty

这里的|->叫"蕴含"，意思是"如果左边成立，那么右边必须成立"。还有一种叫|=>，区别在于：

• |->：重叠蕴含，左边序列结束的同一个周期检查右边
• |=>：非重叠蕴含，左边序列结束的下一个周期开始检查右边

举个例子你就明白了：

// 重叠蕴含：a为高的那个周期，b必须也为高
property overlap;
  @(posedge clk) a |-> b;
endproperty

// 非重叠蕴含：a为高的下一个周期，b必须为高
property non_overlap;
  @(posedge clk) a |=> b;
endproperty

我曾经在一个DMA控制器项目里，就因为搞混了|->和|=>，导致一个握手协议的错误没抓到。仿真怎么跑都过，芯片回来就挂。嗯，从那以后我对这两个符号格外敏感。

属性还可以用not取反：

property p2;
  @(posedge clk) not (a ##1 b);  // 不允许出现a之后b的情况
endproperty

3.4 断言的关键字——assert、assume、cover

有了属性和序列，怎么用呢？三个关键字：

关键字	用途	仿真行为
assert	检查设计是否正确	失败时打印错误，可终止仿真
assume	约束输入激励	形式验证中作为假设，仿真中作为检查
cover	统计覆盖率	记录序列是否发生过

用法很简单：

// 断言：检查正确性
assert property (p1);

// 假设：告诉工具输入必须满足的条件
assume property (@(posedge clk) req |-> ##[1:3] ack);

// 覆盖：看看某个序列是否出现过
cover property (@(posedge clk) a ##1 b ##1 c);

我个人在项目中，一般这样分配：

• 接口协议检查 → 用assert，这是必须保证的
• 输入约束 → 用assume，告诉验证环境别乱给激励
• 关键路径覆盖 → 用cover，看看某些场景有没有跑到

3.5 知识体系总览

说了这么多，咱们用一张图把SVA语法的核心脉络串起来：

你看这张图就清楚了：序列是基础，描述信号的时间行为；属性是规则，把序列组合成检查条件；关键字是动作，告诉工具你要检查、假设还是覆盖。

说白了，写SVA就是三步走：

1. 先想清楚你要检查什么时序行为
2. 用序列把信号的变化描述出来
3. 用属性加上条件，再用assert/assume/cover包装

嗯，SVA的语法入门就聊到这儿。记住：序列是砖，属性是墙，断言是质检员。把这三层关系理清了，写断言就跟搭积木一样自然。