4、SystemVerilog断言(SVA)基础：断言的概念、立即断言与并发断言、assert/assume/cover、序列与属性
各位同学，咱们今天聊聊断言。说实话，我刚入行那会儿，对断言这东西挺不屑的。觉得「代码都写好了，跑仿真不就行了？加什么断言，多此一举」。直到有一次，一个隐蔽的握手协议bug在流片前两周才被发现，差点让整个项目延期。从那以后，我彻底服了——断言不是摆设，它是验证的「眼睛」。
4.1 断言到底是什么？
断言，说白了就是一段检查代码。它盯着你的设计，看某个行为是否符合预期。如果符合，它不说话；一旦不符合，它立刻报警。
我习惯把断言比作「交通摄像头」。你正常开车，它不理你；你闯红灯，咔嚓一张照片，罚单就来了。断言也是这个道理——它只在你出错的时候刷存在感。
断言的核心价值：
- 把设计意图写进代码，而不是留在文档里
- 仿真时自动检查，不用人盯着波形看
- 定位问题快，出错时直接告诉你「哪根信号、哪个时刻、出了什么问题」
嗯，这里要注意：断言不是万能的。它只能检查你写出来的规则，检查不到你没想到的规则。所以断言的质量，直接取决于你对设计理解得有多深。
4.2 立即断言 vs 并发断言
SystemVerilog里断言分两种：立即断言和并发断言。很多新手搞不清区别，我当年也迷糊过一阵子。
4.2.1 立即断言
立即断言，就是「现在立刻检查」。它写在过程块里（比如always块或initial块），执行到这一行时马上判断。
// 立即断言示例
always @(posedge clk) begin
if (valid) begin
assert (data !== 'x)
else $error("data contains X at valid time!");
end
end这段代码的意思是：每当时钟上升沿且valid为高时，立刻检查data里有没有X态。有就报错。
我个人习惯用立即断言做两件事：
- 检查组合逻辑的输出有没有X态
- 检查状态机是否进入了非法状态
注意：立即断言是「事件驱动」的。它只在被触发的那个时刻检查一次。如果你希望持续监控某个信号的行为，得用并发断言。
4.2.2 并发断言
并发断言就不一样了。它像是一个「后台监控进程」，一直在那盯着。它基于时钟沿采样，可以检查跨越多个时钟周期的行为。
// 并发断言示例
property p_req_ack;
@(posedge clk) req |=> ##[1:3] ack;
endproperty
a_req_ack: assert property(p_req_ack);这个断言检查的是：当req拉高后，在接下来的1到3个时钟周期内，ack必须拉高。你看，这涉及时间窗口，立即断言就做不到了。
我记得第一次用并发断言时，写了个很复杂的时序检查，结果仿真跑了一整天都没报错。我还挺得意，觉得设计没问题。后来才发现——我时钟写错了，断言根本没触发。嗯，这是个坑，大家引以为戒。
| 对比项 | 立即断言 | 并发断言 |
|---|---|---|
| 执行方式 | 过程块中立即执行 | 基于时钟沿采样 |
| 时间跨度 | 当前时刻 | 可跨多个时钟周期 |
| 使用场景 | 组合逻辑、X态检查 | 协议时序、握手行为 |
| 性能开销 | 小 | 相对较大 |
4.3 assert / assume / cover 三兄弟
这三个关键字长得像，但分工完全不同。我刚开始也经常搞混，后来用了个比喻才记住：
- assert：检查「设计必须做到的事」。做不到就是bug。
- assume：告诉工具「环境会保证的事」。做不到就是环境有问题。
- cover：记录「这件事有没有发生过」。用来衡量验证的完整性。
4.3.1 assert — 设计必须遵守
assert property(@(posedge clk) !(read & write));这条断言说：读和写不能同时为高。如果仿真中出现了同时为高的情况，那就是设计bug。
4.3.2 assume — 环境必须保证
assume property(@(posedge clk) $stable(rst) || !rst);这条假设说：复位信号在非复位期间必须稳定。如果测试平台让rst乱跳，那就是环境的问题，不是设计的问题。
小技巧：在形式验证中，assume特别重要。它告诉工具「哪些输入组合是合法的」，可以大幅减少无效的状态空间搜索。
4.3.3 cover — 这件事发生过吗？
cover property(@(posedge clk) req ##1 gnt);这条覆盖说：我想知道「请求后紧接着被授权」这个场景有没有被测试到。如果仿真结束，这个cover点从来没被触发过，说明你的测试用例可能漏掉了某个关键场景。
我曾经在一个项目中，写了30多个cover点。仿真跑完后一看，有5个从来没触发过。顺着查下去，发现是某个边界条件根本没测到。你说，如果没有cover，谁能知道验证有漏洞？
4.4 序列与属性
序列（sequence）和属性（property）是SVA的基石。我习惯这么理解：
- 序列：描述「信号怎么变化」——比如req拉高，然后ack拉高。
- 属性：描述「这个变化应该满足什么规则」——比如req拉高后，ack必须在3个周期内拉高。
4.4.1 序列的基本语法
sequence s_req_ack;
req ##1 ack;
endsequence这个序列表示：req为高，然后过一个时钟周期，ack为高。注意那个##1，它表示「延迟一个时钟周期」。
常用的序列操作符：
##n：延迟n个时钟周期##[m:n]：延迟m到n个时钟周期[*n]：重复n次[->n]：非连续重复（goto重复）
4.4.2 属性的基本语法
property p_req_ack_window;
@(posedge clk) req |-> ##[1:3] ack;
endproperty这个属性说：如果req为高，那么在接下来的1到3个周期内，ack必须为高。注意|->和|=>的区别：
|->：重叠蕴含（当前周期就判断）|=>：非重叠蕴含（下一个周期才开始判断）
实战经验：写属性时，我建议先写序列，再包一层属性。这样调试起来方便，序列可以单独拿出来仿真验证。
4.4.3 一个完整的例子
// 序列：请求到授权
sequence s_req_to_gnt;
req ##[1:5] gnt;
endsequence
// 序列：授权后开始传输
sequence s_gnt_to_trans;
gnt ##1 trans_start;
endsequence
// 属性：完整的握手协议
property p_handshake;
@(posedge clk)
s_req_to_gnt |=> s_gnt_to_trans;
endproperty
// 断言
a_handshake: assert property(p_handshake);
// 覆盖
c_handshake: cover property(p_handshake);你看，这样写出来，代码可读性很高。别人一看就知道：哦，这个模块的握手协议是「请求后5个周期内授权，授权后下一个周期开始传输」。
避坑指南：我曾经写过一条断言，检查「读请求后必须读到数据」。仿真跑了一周都没问题，结果形式验证一跑就报错。为什么？因为我的序列里用了##[1:$]，这个「$」表示无限等待。形式验证工具遇到无限时间窗口，直接罢工了。所以，能用有限窗口就别用无限窗口。
4.5 小结
断言这东西，刚开始觉得麻烦，用习惯了就离不开。我现在的习惯是：写RTL之前，先把关键接口的断言写好。这样RTL写完后，仿真一跑，断言自动帮我检查，省心省力。
下一章咱们聊聊「断言的高级用法」，包括多时钟域断言、断言与功能覆盖率的结合。到时候我会分享一个实际项目中的案例——怎么用断言抓到那个藏了三周的bug。