3、SystemVerilog断言基础：立即断言与并发断言，assert/assume/cover 的区别

各位同学，咱们今天聊聊断言。说实话，断言这东西，我刚开始做验证那会儿总觉得是“锦上添花”——有它没它，仿真都能跑。直到有一次，一个很隐蔽的协议错误在流片前两周才被我发现，而那个错误其实早在项目初期就已经埋下了。从那以后，我再也不敢轻视断言了。

SystemVerilog里的断言，说白了就是一段“监视代码”。它帮你盯着信号的变化，一旦出现不符合预期的行为，立刻报警。嗯，这里要注意，断言不是用来“修bug”的，它是用来“抓bug”的。你设计得再完美，总有一些边界情况是你没想到的，断言就是帮你兜底的那张网。

3.1 立即断言：简单粗暴，但很实用

立即断言，顾名思义，就是“立刻”检查。它不关心时间，不关心序列，只关心当前这个时刻的条件是否成立。我个人习惯把它用在组合逻辑检查上，比如状态机的非法状态、数据总线的未知态（X态）等等。

语法很简单：

always_comb begin
    assert (state != 3'b111) else $error("非法状态出现！");
end

你看，就是一个 assert 关键字，后面跟一个条件。条件为真，万事大吉；条件为假，执行后面的 else 语句。这里的 $error 是SystemVerilog内置的打印函数，它会输出错误信息并让仿真继续运行。你也可以用 $fatal 直接终止仿真，看你的需求。

我的小技巧： 在调试阶段，我习惯用 $fatal 让仿真立刻停下来，这样我能第一时间看到出错的波形。到了回归测试阶段，再换成 $error，让仿真跑完所有case，最后统一看log。

立即断言还有一个变种，叫 assume。它和 assert 长得一模一样，但语义完全不同。assert 是“检查”，assume 是“假设”。什么意思呢？

举个例子：

always_ff @(posedge clk) begin
    assume (data_in !== 1'bz) else $error("输入数据不能是高阻态");
end

这个 assume 告诉仿真器：“我假设 data_in 永远不会是高阻态，你帮我验证一下这个假设是否成立。” 如果仿真过程中 data_in 真的变成了高阻态，仿真器会报错。但更重要的是，assume 在形式化验证（Formal Verification）中会被当作“约束条件”，告诉工具：“你只需要考虑 data_in 不是高阻态的那些情况。”

嗯，这里要区分一下：assert 是“我要检查这个对不对”，assume 是“我假设这个是对的，你按这个来验证”。

3.2 并发断言：时间线上的哨兵

并发断言，才是真正体现SystemVerilog断言威力的地方。它关心的是“一段时间内”信号的变化序列。比如，一个握手协议：req拉高后，ack必须在3到5个时钟周期内拉高。这种跨时钟周期的检查，立即断言就无能为力了，得靠并发断言。

并发断言的基本语法是这样的：

property p_handshake;
    @(posedge clk) req |=> ##[3:5] ack;
endproperty

a_handshake: assert property (p_handshake);

我来解释一下：@(posedge clk) 指定了采样时钟。req |=> ##[3:5] ack 的意思是：如果 req 为真，那么从下一个时钟周期开始，在3到5个周期内，ack 必须为真。这个 |=> 是“重叠蕴含”操作符，它表示“如果左边成立，那么右边必须在后续的某个时间点成立”。

并发断言里，assert、assume、cover 这三个关键字都可以用。它们的区别，我总结了一个表格：

关键字 语义 仿真行为 形式化验证行为
assert 断言（检查） 检查属性是否成立，不成立则报错 作为“证明目标”，工具需要证明它永远成立
assume 假设（约束） 检查假设是否成立，不成立则报错 作为“输入约束”，工具只考虑满足假设的输入
cover 覆盖（统计） 统计属性被触发的次数，不报错 不常用，主要用于仿真覆盖率收集

你看，cover 和前面两个完全不同。它不检查对错，只统计“这个序列有没有发生过”。比如，你想知道“req拉高后，ack在恰好第3个周期拉高”这种情况有没有被测试到，就可以写：

property p_exact_3;
    @(posedge clk) req |=> ##3 ack;
endproperty

c_exact_3: cover property (p_exact_3);

仿真结束后，你可以在覆盖率报告里看到这个 cover 被触发了多少次。如果一次都没触发，说明你的测试用例没覆盖到这个边界情况，得补case。

我曾经踩过的坑： 有一次，我写了一个并发断言，用 assert 检查一个很复杂的协议序列。仿真跑了一整天，0个错误。我心想“完美！”。结果后来发现，那个断言的条件写错了，导致它永远都不会被触发。从那以后，我养成了一个习惯：每个 assert 旁边，一定配一个 cover，先确认断言确实被触发了，再去看有没有错误。

3.3 assert / assume / cover 的实战选择

说了这么多，到底什么时候用哪个？我个人的经验是这样的：

  • 用 assert 的场景： 检查设计内部的协议、状态机跳转、数据通路。比如“写操作时，写使能必须为高”、“FIFO满时不能写入”。这些是设计必须遵守的规则，错了就是bug。
  • 用 assume 的场景： 约束测试平台的输入。比如“输入数据不能为X态”、“地址必须对齐”。这些不是设计的问题，而是测试平台应该保证的。用 assume 可以帮你尽早发现测试平台的bug。
  • 用 cover 的场景： 衡量功能覆盖率。比如“读操作和写操作交替发生”、“总线进入空闲状态”。这些不一定是bug，但如果你没测到，说明你的测试用例不够全面。

你想想看，这三个关键字其实对应了验证的三个维度：正确性（assert）、合法性（assume）、完备性（cover）。一个好的验证方案，三者缺一不可。

3.4 一个完整的例子

最后，我给大家看一个我在项目中实际用过的例子。这是一个简单的AXI4-Stream握手检查：

// 假设：TVALID 和 TREADY 不能同时为X态
assume_inputs: assume property (
    @(posedge clk) disable iff (rst_n)
    !$isunknown({tvalid, tready})
) else $error("输入信号包含X态");

// 断言：TVALID 拉高后，TREADY 必须在100个周期内拉高
assert_handshake: assert property (
    @(posedge clk) disable iff (rst_n)
    $rose(tvalid) |-> ##[1:100] tready
) else $error("握手超时");

// 覆盖：记录 TVALID 和 TREADY 同时为高的周期数
cover_both_high: cover property (
    @(posedge clk) tvalid && tready
);

你看，三个断言各司其职。assume 保证输入干净，assert 检查协议正确，cover 统计握手成功的情况。这样一套下来，我对这个接口的验证信心就足了很多。

好了，关于断言的基础就讲到这里。记住，断言不是写给别人看的，是写给你自己用的。你花10分钟写一个断言，可能在未来帮你省下10个小时的调试时间。这笔账，怎么算都划算。

← 上一章 📖 返回目录 下一章 →