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

好，咱们正式开始啃SVA这块硬骨头。说实话，我刚接触SVA那会儿，觉得这东西不就是写几个检查条件嘛，有啥难的？结果第一次在项目里写断言，就被现实狠狠教育了一顿——仿真跑了两天，最后发现是我自己写的断言语法错了，根本没生效。嗯，从那以后我就老老实实把语法基础打扎实了。

今天咱们就聊聊SVA最核心的三个东西：基本结构、序列与属性、以及三个关键字。你把这几个搞明白，后面写断言基本就顺了。

2.1 SVA的基本结构

SVA说白了就是一段描述时序关系的代码。它的基本骨架长这样：

// 最简单的SVA结构
property my_property;
    @(posedge clk) a |-> b ##1 c;
endproperty

assert property (my_property);

你看，就三部分：

• property：定义你要检查的时序行为
• 时序表达式：用@(posedge clk)指定时钟，用|->、##等运算符描述信号关系
• 断言关键字：告诉工具你要assert（验证）、assume（假设）还是cover（覆盖）

我个人习惯把property单独拎出来写，而不是直接塞在assert里面。为什么？因为后期维护的时候，你一眼就能看到这个property是干啥的，改起来也方便。我在一个项目里见过有人把几十行断言全写在assert后面，那代码简直没法看。

2.2 序列(sequence)与属性(property)

这两个概念容易搞混。我简单说说我的理解：

• 序列（sequence）：描述信号在时钟周期上的变化。比如“a拉高后，下一个周期b拉高”。它只描述事件，不判断对错。
• 属性（property）：在序列的基础上加上逻辑判断。比如“只要a拉高，下一个周期b必须拉高”。它是有对错之分的。

举个例子你就明白了：

// 序列：只描述事件
sequence s_req_ack;
    @(posedge clk) req ##1 ack;
endsequence

// 属性：加上判断
property p_req_ack;
    @(posedge clk) req |-> ##1 ack;
endproperty

// 使用
assert property (p_req_ack);

你看，sequence只是说“req之后一个周期有ack”，而property说“只要req出现，下一个周期必须要有ack”。区别就在这个|->上，它叫蕴含操作符，意思是“如果左边成立，那么右边必须成立”。

我曾经在一个项目里犯过傻——直接用sequence去assert，结果工具报错。后来才明白，sequence本身没有“对错”的概念，它只是描述。你得把它包在property里，加上蕴含或者别的逻辑，才能做断言。

2.3 三个关键字：assert, assume, cover

这三个关键字，每个都有不同的用途。我分别说说：

2.3.1 assert —— 验证

这是最常用的。它的意思是“我要求这个行为必须成立，如果不成立，就是bug”。

assert property (p_req_ack);

仿真时如果req拉高后没看到ack，工具就会报错。我在项目中一般把assert用在关键接口上，比如握手协议、状态机跳转、数据完整性检查这些地方。

2.3.2 assume —— 假设

这个有点意思。assume不是用来检查设计的，而是用来约束输入的。它告诉工具：“我假设输入信号会按照这个行为来，你别给我乱来。”

assume property (@(posedge clk) !(req & ack));

这条假设的意思是：req和ack不能同时为高。如果仿真时输入违反了这条，工具会报warning，但不会说设计有bug。为什么？因为这是你给环境加的约束，不是设计本身的问题。

我记得有一次做形式化验证，环境里忘了加assume，结果工具跑出来一堆假失败——都是因为输入乱跳导致的。后来加上assume，问题全消了。所以assume在形式化验证里特别重要，它帮你把输入空间限定在合理范围内。

2.3.3 cover —— 覆盖

cover用来检查“某个行为是否发生过”。它不判断对错，只统计覆盖率。

cover property (s_req_ack);

这条cover会统计“req之后一个周期ack出现”这个序列被触发了多少次。如果覆盖率低，说明你的测试用例没覆盖到这条路径。

我个人习惯在写完assert之后，顺手加一条cover。为什么？因为有时候断言通过了，但你可能根本没触发到关键路径。cover能帮你发现测试的盲区。

2.4 三者配合使用

实际项目中，这三个关键字经常一起出现。我给你看个典型的例子：

// 假设：输入不会同时有效
assume property (@(posedge clk) !(req & gnt));

// 验证：请求后必须得到授权
assert property (@(posedge clk) req |-> ##[1:3] gnt);

// 覆盖：记录请求到授权的延迟分布
cover property (@(posedge clk) req ##0 gnt);
cover property (@(posedge clk) req ##1 gnt);
cover property (@(posedge clk) req ##2 gnt);
cover property (@(posedge clk) req ##3 gnt);

你看，assure约束输入，assert检查设计，cover统计覆盖。三者各司其职，缺一不可。

嗯，今天的内容就到这儿。SVA的语法其实不难，难的是怎么把时序关系用SVA准确表达出来。下一章咱们聊聊更复杂的序列操作符，比如重叠蕴含、非重叠蕴含、还有各种延迟范围。到时候我会拿实际项目里的例子来讲，保证你听完就能上手写。

记住：写断言不是为了写而写，是为了帮你发现bug。所以，从今天开始，每写一段RTL，顺手加几条断言。养成习惯后，你会发现调试时间能省一半。