第二章：断言与反例分析

断言（Assertion）的本质

断言这东西，说白了就是你在设计里埋下的「哨兵」。我刚开始做形式化验证时，总觉得断言是可有可无的装饰品。直到有一次，一个隐蔽的地址越界问题在仿真里跑了三天都没抓到，换成形式化验证加断言，十分钟就揪出来了。

断言的本质是什么？我个人的理解是——它是对设计行为的强制性约束。你告诉工具：「这里不能出现这种情况，如果出现了，就是 bug。」

常见的断言类型，我归纳为三类：

• 安全断言（Safety）：检查「坏事永远不会发生」。比如 FIFO 满时不能写，空时不能读。
• 活性断言（Liveness）：检查「好事终究会发生」。比如请求发出后，最终一定会收到响应。
• 时序断言（Timing）：检查信号之间的相对时序关系。比如 valid 拉高后，ready 必须在 3 个周期内拉高。

反例（Counterexample）的结构

反例是什么？就是工具找到的一条「违规路径」。它告诉你：从某个初始状态出发，经过一系列操作，最终触发了你的断言。

一个标准的反例，通常包含三个部分：

1. 初始状态：所有寄存器、存储器的初始值。嗯，这里要注意，初始状态不一定是全零，也可能是你指定的复位状态。
2. 输入序列：每个时钟周期输入端口上的值。这是反例的核心，它展示了触发 bug 的「作案过程」。
3. 内部状态变化：关键寄存器和内部信号在每个周期的值。这部分帮你理解「为什么输入序列会导致断言失败」。

我记得有一次，一个同事盯着反例波形看了两个小时，死活找不到问题。我过去一看，他一直在看输出信号，完全忽略了内部状态。其实反例里最值钱的信息，往往藏在那些中间寄存器的变化里。

如何从反例波形中提取关键信息

反例波形，说白了就是一张「犯罪现场还原图」。但很多人拿到波形后，只会盯着看，不知道从哪里下手。我总结了一套「三步法」：

第一步：定位触发时刻

找到断言失败的那个时钟周期。波形上通常会有一个标记，或者工具会告诉你具体的时间点。这个时刻就是「案发现场」。

第二步：检查输入条件

看看触发时刻的输入信号是什么状态。是不是某个输入组合恰好满足了断言的条件？比如断言检查的是「当 A=1 且 B=1 时，C 必须在下一周期为 1」，结果你发现触发时刻 A=1、B=1，但下一周期 C=0。那问题就出在 C 的生成逻辑上。

第三步：反向追踪根因

从触发时刻开始，沿着数据路径往前追。看看是哪个寄存器的值不对，或者哪条组合逻辑算错了。我曾经遇到过一个案例，反例显示一个计数器在特定条件下少加了 1。往前追了 5 个周期才发现，是复位逻辑里有个优先级写反了。

知识体系结构图

实战案例：一个简单的 FIFO 断言

来看一个我实际处理过的例子。假设我们有一个 FIFO，深度为 8。我们写了一个断言：

// 断言：FIFO 满时不能写
assert property (
  @(posedge clk) 
  disable iff (!rst_n)
  (fifo_full |-> !wr_en)
);

工具返回了一个反例。波形显示：

周期	wr_en	fifo_full	wr_ptr	rd_ptr	备注
T0	1	0	0	0	写入第一个数据
T1	1	0	1	0	继续写入
...	...	...	...	...	...
T7	1	1	7	0	断言失败！满时还在写

你看，反例清晰地展示了：从 T0 到 T7，wr_en 一直为高，rd_ptr 从未变化（没有读操作）。到了 T7 时，fifo_full 已经拉高，但 wr_en 仍然为 1，触发了断言。

这个案例告诉我们什么？反例不仅告诉你「哪里错了」，还告诉你「怎么错的」。从波形里，我们能看到：问题出在写使能逻辑没有检查满标志，或者检查了但优先级处理有误。

可可精品资料库