芯片形式化验证与UVM协同验证 - 第4节
一、SVA 语法入门：从零开始写断言
大家好，我是你们的芯片验证讲师。今天咱们聊聊形式化验证里最基础也最核心的东西——SVA（SystemVerilog Assertions）。
说实话，我刚入行那会儿，觉得断言就是写几个检查点，没啥技术含量。直到有一次，一个 bug 在仿真里跑了三天都没抓到，最后用形式化工具一跑，十分钟就定位到了问题。嗯，从那以后，我再也不敢小看 SVA 了。
1.1 什么是 SVA？
SVA 是 SystemVerilog 里专门用来描述时序行为的语言。说白了，就是告诉工具：「信号 A 拉高后，信号 B 必须在 3 个时钟内拉高，否则就是 bug」。
我个人习惯把 SVA 分成三块：
- 序列（sequence）：描述信号在时间轴上的行为模式
- 属性（property）：把序列组合成完整的检查规则
- 断言（assert）：把属性挂到设计上，让工具去验证
核心思想：SVA 不是用来「写代码」的，而是用来「描述期望」的。你描述得越精确，工具抓 bug 就越准。
1.2 最简单的 SVA 例子
先看一个最基础的断言：
// 检查：当 rst_n 拉高后，data_valid 必须在 5 个时钟内拉高
property p_data_valid;
@(posedge clk)
$rose(rst_n) |-> ##[1:5] data_valid;
endproperty
a_data_valid: assert property(p_data_valid);这里我解释一下：
$rose(rst_n)检测 rst_n 的上升沿|->是蕴含操作符，表示「如果左边成立，那么右边必须成立」##[1:5]表示延迟 1 到 5 个时钟周期
我在项目中遇到过类似场景：有个同事写了个 ##[0:5]，结果 rst_n 刚拉高 data_valid 就拉高了，但工具报错。为啥？因为 ##[0] 表示同一拍，而 rst_n 和 data_valid 的时序关系不允许同一拍。这种细节，不踩坑真的记不住。
二、序列（sequence）与属性（property）
2.1 序列：时序行为的「积木块」
序列是 SVA 里最小的可复用单元。你可以把它理解成乐高积木——先搭好小模块，再拼成大结构。
举个例子：
// 定义一个序列：req 拉高后，gnt 必须在 2-4 个时钟内拉高
sequence s_req_gnt;
@(posedge clk)
$rose(req) ##[2:4] $rose(gnt);
endsequence这里有几个关键点：
##[2:4]是固定延迟范围，不能写成##[2:4:2]（没有步长概念）$rose()检测上升沿，$fell()检测下降沿，$stable()检测不变- 序列可以嵌套：
s_req_gnt ##[1:3] s_done
我的小技巧：写序列时，尽量把「触发条件」和「检查条件」分开。比如上面例子，触发条件是 $rose(req)，检查条件是 $rose(gnt)。这样后期维护时，改一个不影响另一个。
2.2 属性：把序列「包装」成规则
属性是序列的「外壳」。它告诉工具：这个检查是「必须成立」还是「禁止出现」。
常见的属性类型：
| 类型 | 关键字 | 含义 | 例子 |
|---|---|---|---|
| 蕴含 | |-> | 左边成立时，右边必须成立 | a |-> b |
| 蕴含（重叠） | |=> | 左边结束时，右边开始 | a ##1 b |=> c |
| 禁止 | not | 指定行为不能发生 | not (a ##1 b) |
| 始终 | always | 整个仿真期间都检查 | always (a |-> b) |
我曾经犯过一个错：把 |-> 和 |=> 搞混了。前者是「左边成立时，右边立即开始检查」，后者是「左边结束后，右边才开始」。在形式化验证里，这个区别会导致完全不同的结果。你想想看，如果时序差了一拍，工具可能报一堆假错。
三、断言（assert）与覆盖（cover）
3.1 断言：你的「电子警察」
断言就是挂在设计上的检查器。形式化验证里，断言是核心——工具会穷举所有可能的状态，看有没有违反断言的情况。
断言有三种：
- 立即断言：
assert (a == b);只检查当前时刻 - 并发断言：
assert property (p);检查时序行为 - 假设：
assume property (p);告诉工具「输入必须满足这个条件」
注意：形式化验证里，assume 和 assert 同样重要。假设写少了，工具会探索不可能的状态；假设写多了，又会漏掉真实 bug。我刚开始做形式化时，就吃过「假设太强」的亏——工具跑得飞快，但啥 bug 都没找到。后来才发现，我把输入约束得太死了。
3.2 覆盖：看看你的验证「覆盖率」
覆盖（cover）用来检查「某些场景是否被验证到了」。形式化验证里，覆盖点特别有用——它能告诉你，工具是否真的探索到了你关心的行为。
// 检查：是否出现过 req 拉高后 3 个时钟内 gnt 拉高的场景
cover property (@(posedge clk) $rose(req) ##[1:3] $rose(gnt));我个人习惯在写断言的同时，顺手写几个覆盖点。这样跑完形式化后，一看覆盖报告就知道：「哦，这个场景没覆盖到，说明我的约束可能有问题」。
四、SVA 在形式化中的特殊用法
4.1 形式化 vs 仿真：SVA 的「性格」变了
同样的 SVA，在仿真和形式化里，行为可能完全不同。为啥？因为形式化工具是「数学证明」，不是「跑波形」。
举个例子：
// 仿真里：检查每个时钟周期
assert property (@(posedge clk) a |-> b);
// 形式化里：工具会证明「在所有可能的输入序列下，a 成立时 b 是否一定成立」形式化工具会考虑所有可能的延迟、所有可能的输入组合。所以，SVA 里的一些「模糊」写法，在形式化里可能出问题。
4.2 形式化中要避免的 SVA 写法
| 写法 | 仿真中 | 形式化中 |
|---|---|---|
##[0:$] |
可以，但可能跑很久 | 工具会爆炸（无限状态） |
s_eventually |
可以 | 慎用，可能导致状态爆炸 |
within |
可以 | 尽量用固定范围替代 |
嵌套的 not |
可以 | 可能产生反例难理解 |
避坑指南：我曾经写过一个 ##[0:$] 的断言，形式化工具跑了 48 小时没出结果。后来改成 ##[0:10]，5 分钟就搞定了。记住：形式化里，时间范围越精确，工具越快。
4.3 形式化中的「假设驱动」思维
形式化验证有个特点：你写的假设（assume）决定了工具探索的空间。SVA 在这里的角色，不只是「检查器」，更是「约束器」。
我常用的套路：
- 先写
assume约束输入（比如：rst_n 不能连续拉高两次） - 再写
assert检查输出（比如：gnt 必须在 req 后 5 拍内拉高） - 最后写
cover确认场景被覆盖
你想想看，如果输入约束没写好，工具可能去探索「rst_n 每拍都翻转」这种不现实的情况，白白浪费算力。
五、本章知识体系图
下面这张图，是我自己总结的 SVA 在形式化中的知识结构：
这张图把 SVA 在形式化中的核心要素串起来了。从左到右，从序列到属性再到断言/覆盖，每一步都是递进关系。底部是形式化验证的三个核心原则，我每次写断言前都会默念一遍。
六、本章小结
好了，这一章的内容就到这里。咱们聊了 SVA 的语法基础、序列和属性的区别、断言和覆盖的用法，还有形式化中的特殊注意事项。
说实话，SVA 看起来简单，但真正用好它，需要大量的实践。我建议你从最简单的断言开始写，慢慢增加复杂度。遇到问题别怕，形式化工具会告诉你哪里错了——有时候，错误信息本身就是最好的学习材料。
下一章，我们会深入形式化验证的数学基础，聊聊「有界模型检查」和「无界模型检查」到底是怎么回事。到时候见！