2、SVA语法速览：立即断言与并发断言、序列与属性

各位同学，咱们今天聊聊SVA（SystemVerilog Assertions）的语法基础。说实话，我刚接触断言那会儿，也觉得这东西有点绕。但用久了你会发现，它其实就是一套描述「电路行为应该是什么样」的语言。

我个人习惯把SVA分成两大块：立即断言和并发断言。这两兄弟各有各的脾气，咱们一个一个说。

2.1 立即断言：说干就干的急性子

立即断言，顾名思义，就是立刻执行。它不依赖时钟，也不管时序，你写在哪，它就在哪执行。

语法很简单：

label: assert (expression) else $error("消息");

举个例子：

always_comb begin
    valid_assert: assert (data_valid && !busy) 
        else $fatal("data_valid和busy不能同时为高");
end

我在项目中遇到过一个问题：有人把立即断言写在always_ff里，结果仿真跑得巨慢。为什么？因为每个时钟沿都触发，而且断言本身也有开销。后来我改成always_comb，只在组合逻辑里用立即断言，性能就好多了。

2.2 并发断言：按节奏办事的稳重派

并发断言就不一样了。它依赖时钟，只在时钟沿采样。你想想看，时序电路的行为，是不是得按节拍来？

基本格式：

label: assert property (property_expr) else $error("消息");

其中property_expr就是我们要定义的属性。比如：

a1: assert property (@(posedge clk) req |-> ##2 ack);
// 意思是：req拉高后，2个时钟周期内ack必须拉高

嗯，这里要注意：并发断言默认是多线程的。每个时钟沿都会启动一个新的断言检查线程。如果你不小心，可能会产生大量线程，把仿真器跑崩。我建议在顶层控制一下断言密度，别一股脑全开。

2.3 序列：描述信号的「时间模式」

序列（sequence）是SVA的核心。它描述的是信号在一段时间内的变化模式。

定义序列：

sequence s1;
    @(posedge clk) a ##1 b ##1 c;
endsequence

这个序列的意思是：在连续3个时钟沿，a、b、c依次为高。

常用的操作符：

操作符	含义	示例
##n	延迟n个时钟周期	a ##2 b
##[m:n]	延迟范围	a ##[1:3] b
[*n]	重复n次	a[*3]
[->n]	非连续重复	a[->2]

我记得有个项目，验证DMA传输完成信号。用序列写起来特别优雅：

sequence dma_done_seq;
    @(posedge clk) dma_start ##[5:100] dma_done;
endsequence

说白了，序列就是给信号拍「时间照片」。你只要把期望的行为拍下来，剩下的交给SVA去检查。

2.4 属性：序列的「逻辑包装」

属性（property）是在序列外面包了一层逻辑。它告诉工具：这个序列什么时候该成立，什么时候可以忽略。

属性定义：

property p1;
    @(posedge clk) disable iff (rst) 
        req |-> ##[1:3] gnt;
endproperty

这里disable iff (rst)的意思是：复位时禁用这个属性检查。这个太实用了，不然复位期间一堆误报，你根本看不完。

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

• |->：重叠蕴含（当前周期就检查后续）
• |=>：非重叠蕴含（下一个周期才开始检查）

举个例子区分一下：

// 重叠蕴含：a为高的同一周期，b必须为高
a |-> b

// 非重叠蕴含：a为高的下一个周期，b必须为高
a |= b

2.5 知识体系总览

说了这么多，咱们用一张图把关系理清楚：

这张图把关系说得很清楚：SVA分两大派，立即断言和并发断言。并发断言又依赖序列和属性。序列描述「怎么做」，属性描述「什么时候做」。两者配合，就能写出强大的断言。

2.6 实战建议

最后给几个实战建议：

1. 能用并发断言就别用立即断言。并发断言更贴近时序电路的本质，而且支持形式化验证。
2. 序列尽量短小精悍。一个序列别超过5个操作符，否则可读性太差。我见过有人写20个##的序列，那简直是天书。
3. 属性里一定要加disable iff。不然复位期间一堆误报，你根本分不清真假。
4. 断言覆盖率要单独收集。很多工具默认不收集断言覆盖率，你得手动开一下。

好了，这一章就到这里。记住一句话：断言不是用来找bug的，是用来证明你的设计是对的。心态摆正了，学起来就快了。

可可精品资料库