3. SystemVerilog断言基础：断言的概念、立即断言与并发断言、assert/assume/cover关键字、简单断言示例

好，咱们今天聊聊断言。说实话，我刚入行那会儿，觉得断言这东西可有可无——代码能跑通不就行了？直到有一次，一个隐蔽的时序bug在仿真里溜了过去，流片回来才发现，那叫一个追悔莫及。从那以后，我养成了一个习惯：写代码必写断言，就像出门必带钥匙一样自然。

3.1 断言到底是什么？

断言，说白了就是一段“自检代码”。它帮你盯着设计里的关键行为，一旦出问题就立刻报警。你想想看，一个复杂的芯片设计，成千上万条信号线，靠人眼去波形图里找bug？那简直是海底捞针。

断言的作用就是：把“应该发生的事”和“不该发生的事”写下来，让工具替你去检查。

我个人习惯把断言分成两类：

  • 正确性断言：检查设计是否满足预期行为。比如“握手信号来了之后，数据必须在3个时钟内被取走”。
  • 非法状态断言：检查是否出现了不该出现的情况。比如“状态机不应该同时处于IDLE和BUSY状态”。

核心思想：断言不是用来“证明”设计是对的，而是用来“发现”设计是错的。你永远无法证明没有bug，但你可以用断言让bug无处藏身。

3.2 立即断言 vs 并发断言

这两个概念，我当年学的时候也绕了一阵。其实区别很简单：

特性 立即断言 并发断言
执行时机 执行到该行代码时立即检查 基于时钟沿，在仿真过程中持续监控
使用场景 组合逻辑、函数内部、initial块 时序逻辑、跨时钟域、协议检查
语法形式 assert (expression) assert property (property_expr)
能否用时序表达式 不能（只有组合逻辑） 能（支持 ##1, |=>, s_until 等）

立即断言，就像你在代码里埋了个地雷——踩到就炸。它只检查当前时刻的值，不关心过去和未来。

// 立即断言示例
always_comb begin
  // 我习惯在状态机解码后面加这个
  assert (state inside {IDLE, BUSY, DONE})
    else $error("状态机进入非法状态: %0d", state);
end

并发断言，则像是一个哨兵，站在时钟边上，每个时钟沿都看一眼。它能表达“过去发生了什么”、“未来应该发生什么”这类时序关系。

// 并发断言示例
// 检查：req拉高后，2~5个时钟内必须收到ack
assert property (@(posedge clk) 
  req |=> ##[2:5] ack)
  else $error("req后未在2~5周期内收到ack");

我的经验：能用并发断言就别用立即断言。并发断言更强大，而且能生成覆盖率数据。立即断言我只用在组合逻辑的“防呆”检查上。

3.3 assert / assume / cover 三兄弟

这三个关键字，功能不同但相辅相成。我经常把它们比作：

  • assert：警察——抓违规的
  • assume：编剧——规定输入剧本
  • cover：记者——记录精彩瞬间

3.3.1 assert — 验证正确性

这是最常用的。assert失败意味着设计有bug。在仿真中，assert失败默认会打印一条消息，但不会停止仿真（除非你设置了$fatal）。

// 检查：fifo空时不能读
assert property (@(posedge clk) 
  !fifo_empty |=> rd_en)
  else $error("fifo空时尝试读取");

3.3.2 assume — 约束输入环境

assume和assert语法完全一样，但语义不同。assume是告诉工具：“我保证外部环境会满足这个条件，你不需要验证它，但形式化验证时请把它当作约束。”

我曾经在一个项目中吃过亏——没有加assume，结果形式化工具花了三天三夜去遍历一些根本不可能出现的输入组合。加了assume之后，十分钟就跑完了。

// 假设：外部输入的addr不会超过0xFF
assume property (@(posedge clk) 
  addr <= 8'hFF)
  else $error("addr超出范围");

注意：assume在仿真中行为和assert一样（失败会报错），但在形式化验证中，它会被当作“环境约束”。滥用assume可能会掩盖真实的bug——你想想看，如果你assume了“输入永远正确”，那输出错了也怪不到输入头上。

3.3.3 cover — 收集覆盖率

cover用来记录“某个事件是否发生过”。它不会报错，只会默默计数。在验证的最后阶段，我会用cover来确认：所有重要的场景都已经被覆盖到了。

// 覆盖：是否出现过“写满又读空”的场景
cover property (@(posedge clk) 
  fifo_full ##1 fifo_empty);

嗯，这里要注意：cover和assert可以共用同一个property。我经常先写一个assert，然后复制一行改成cover——既能检查正确性，又能收集覆盖率。

3.4 简单断言示例：一个握手协议

咱们来看一个完整的例子。假设有一个简单的握手协议：valid拉高后，ready必须在3个时钟内拉高，否则超时。

module handshake_checker (
  input clk,
  input rst_n,
  input valid,
  input ready
);

  // 1. 立即断言：valid和ready不能同时为X态
  always_comb begin
    assert (!$isunknown(valid) && !$isunknown(ready))
      else $error("valid或ready出现X态");
  end

  // 2. 并发断言：valid拉高后，ready必须在3周期内拉高
  property p_handshake_timeout;
    @(posedge clk) disable iff (!rst_n)
    valid |=> ##[1:3] ready;
  endproperty

  assert property (p_handshake_timeout)
    else $error("握手超时：valid后3周期内未收到ready");

  // 3. 覆盖：记录成功握手的次数
  cover property (@(posedge clk) 
    valid && ready);

  // 4. 假设：valid不能连续拉高超过10个周期
  assume property (@(posedge clk) 
    $rose(valid) |=> valid[*1:10] ##0 !valid)
    else $error("valid连续拉高超过10周期");

endmodule

你看，一个简单的模块，用断言就把所有关键行为都锁死了。我个人习惯在写RTL的同时就把断言写好——等代码写完了再补断言，往往会漏掉很多边界情况。

3.5 知识体系总览

下面这张图，是我自己总结的断言知识框架。每次带新人，我都会先让他们看这张图——把概念理清了，后面学起来就快了。

SystemVerilog 断言知识体系 立即断言 并发断言 覆盖断言 组合逻辑检查 执行到即检查 不支持时序表达式 时序逻辑检查 基于时钟沿持续监控 支持 ##1, |=> 等 记录事件发生 不报错只计数 用于覆盖率分析 assert assert / assume cover 三者结合：assert 抓bug + assume 定环境 + cover 看覆盖

我的建议：刚开始学断言，别贪多。先把assert和cover用好，assume可以等接触形式化验证时再深入。记住一个原则——宁可误报，不可漏报。断言写得宽松了，bug就溜过去了；写得严格了，顶多花点时间排查误报。

好了，这一章的内容就到这里。断言这东西，光看是学不会的，得动手写。我建议你找个自己写过的模块，试着加几个断言上去，跑一遍仿真看看效果——相信我，你会爱上这种“让工具替你找bug”的感觉。

可可精品资料库

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