1. 断言基础：什么是断言？断言在验证中的角色、断言语言（SVA）概述

好，咱们直接进入正题。今天聊断言，也就是 Assertion。

你可能听过一句话：「断言是验证的灵魂」。这话有点夸张，但也不无道理。我做了十几年验证，见过太多项目因为没用好断言，最后 debug 到崩溃。嗯，咱们今天就把这个基础打牢。

1.1 什么是断言？

断言，说白了就是一句话：「我赌这里一定成立，如果不成立，你就报错」。

举个例子。你写了一个 FIFO，深度 16。你心里清楚，写指针和读指针的差值不能超过 16。但你怎么保证？靠人眼 review？靠仿真波形慢慢看？

断言就是帮你自动盯住这个条件的工具。你写一句：

assert (wr_ptr - rd_ptr) <= 16;

仿真时一旦越界，工具立刻告诉你：「喂，这里出事了！」

我个人习惯把断言理解为「设计契约」。你告诉工具：我的设计应该满足什么行为。工具帮你盯着，一旦违约，立刻报警。

1.2 断言在验证中的角色

断言到底有什么用？我总结了三句话：

• 抓 bug 更快 —— 不用等到波形出来再人眼比对
• 定位更准 —— 断言直接告诉你哪里错了，而不是「输出不对」
• 文档即验证 —— 断言本身就是设计规范的可执行版本

我在项目中遇到过一件事。一个同事花了三天 debug 一个总线协议问题，最后发现是某个握手信号少拉了一个周期。如果当时写了断言，十分钟就能定位。你想想看，这效率差了多少？

断言在验证流程中的角色，可以用下面这张图来理解：

这张图想表达什么？断言不是孤立存在的。它从设计规范中来，服务于仿真、形式验证和覆盖率分析，最终帮你快速定位 bug。

1.3 断言语言（SVA）概述

SVA，全称 SystemVerilog Assertions。它是 SystemVerilog 的一部分，专门用来描述断言。

为什么要有专门的断言语言？直接用 if-else 不行吗？

嗯，这里要注意。if-else 是过程性语句，你得写在 always 块里，还得自己控制采样时机。而 SVA 是声明性的，你只需要描述「什么条件应该成立」，工具自动帮你处理采样和报告。

SVA 的核心概念其实不多，就这几个：

概念	说明	示例
立即断言	组合逻辑检查，写在过程块中	assert (a && b);
并发断言	基于时钟周期的时序检查	assert property (@(posedge clk) a |-> b);
序列	描述信号在多个周期内的行为	sequence s; a ##1 b ##1 c; endsequence
属性	对序列施加逻辑条件	property p; @(posedge clk) s |-> d; endproperty

我刚开始学 SVA 时，觉得序列和属性这两个概念特别绕。后来想通了：序列描述「发生了什么」，属性描述「应该怎样」。就这么简单。

来看一个完整的例子：

// 序列：req 拉高后，2~5 个周期内 ack 必须拉高
sequence req_ack_seq;
  req ##[2:5] ack;
endsequence

// 属性：每次 req 拉高，最终 ack 必须拉高
property req_ack_prop;
  @(posedge clk)
  $rose(req) |-> ##[2:5] $rose(ack);
endproperty

// 断言
assert property (req_ack_prop)
  else $error("req 后 ack 未在 2~5 周期内拉高！");

1.4 断言的两大类型

SVA 的断言分两种，咱们得搞清楚：

• 立即断言（Immediate Assertion）：像 if 一样，执行到那行就检查。不能跨周期。
• 并发断言（Concurrent Assertion）：基于时钟，可以描述跨多个周期的行为。这才是 SVA 的精髓。

举个例子你就明白了：

// 立即断言：检查当前值
always_comb begin
  assert (state != IDLE || ready == 1)
    else $error("IDLE 状态下 ready 必须为 1");
end

// 并发断言：检查跨周期行为
assert property (@(posedge clk)
  $rose(valid) |-> ##2 $rose(ready));

我个人习惯：组合逻辑用立即断言，时序逻辑用并发断言。这样分工明确，不容易乱。

1.5 断言的价值：一个真实案例

说个我自己的经历。几年前做一个 PCIe 控制器，DMA 模块有个要求：descriptor 读完后，必须在 16 个周期内开始数据传输。

这个要求写在设计文档里，但没人写断言。结果验证阶段发现性能不达标，查了整整一周，最后发现是 DMA 偶尔会延迟 17 个周期才启动传输。

如果当时写了这句断言：

assert property (@(posedge clk)
  desc_done |-> ##[1:16] data_start);

仿真跑一轮就能发现，根本不用等一周。你想想看，这就是断言的价值。

好了，这一章咱们把断言是什么、有什么用、SVA 长什么样都过了一遍。下一章我会带你手写第一个断言，咱们从最简单的开始。