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

1.1 断言到底是什么？

先说说我对断言的理解。说白了，断言就是一段代码，用来检查你的设计是不是按预期工作。它不像普通的 testbench 代码那样产生激励，而是像个「哨兵」一样，时刻盯着信号的变化。

我记得刚入行时，带我的老工程师跟我说过一句话：「断言不是用来证明设计是对的，而是用来证明设计是错的。」这句话我到现在都觉得特别精辟。你想想看，验证的本质不就是找 bug 吗？断言就是帮你自动找 bug 的工具。

1.2 断言在验证中的角色

断言在验证流程里到底扮演什么角色？我把它总结为三个核心作用：

• 实时监控：仿真过程中，断言就像个「电子眼」，时刻盯着关键信号。一旦出现异常，立刻报警。我在项目中遇到过，一个复杂的 AXI 总线协议，如果没有断言，光靠看波形找协议违例，那简直是噩梦。
• 设计文档活起来：很多设计文档写得很详细，但没人看。断言就不一样了，它把文档里的「应该」变成了可执行的检查。比如「读请求发出后，必须在 16 个周期内返回数据」，写成断言后，仿真器会帮你盯着。
• 调试加速器：没有断言的时候，发现 bug 往往要等到输出结果出错。有了断言，bug 在发生的瞬间就被抓住了。我曾经调试一个 bug，从波形上看，错误信号出现后过了 2000 个周期才导致最终输出错误。如果没有断言，我得倒推 2000 个周期去找根因，那工作量...嗯，你懂的。

验证阶段	断言的作用	我的经验
模块级验证	检查接口协议、状态机跳转	这里断言最有效，bug 发现率最高
系统级验证	检查跨模块交互、数据一致性	需要精心设计，否则容易误报
形式化验证	作为 property 输入给工具	断言质量直接决定形式化验证效果

1.3 断言语言概述：SVA vs PSL

目前主流的断言语言就两种：SVA（SystemVerilog Assertions）和 PSL（Property Specification Language）。我个人几乎只用 SVA，因为 SystemVerilog 已经是行业标准了。但 PSL 在某些遗留项目里还能见到，简单了解一下没坏处。

SVA（SystemVerilog Assertions）

SVA 是 SystemVerilog 标准的一部分，2005 年就纳入了 IEEE 标准。它的语法和 Verilog/SystemVerilog 高度融合，写起来很顺手。

一个简单的 SVA 例子：

// 检查：当 valid 拉高时，data 必须在 1 个周期内有效
property p_valid_data;
  @(posedge clk)
  valid |-> ##[1:1] data_valid;
endproperty

assert property (p_valid_data) else
  $error("valid 拉高后 data 未在 1 周期内有效");

PSL（Property Specification Language）

PSL 比 SVA 出现得更早，最初是 IBM 开发的。它的语法更接近数学逻辑，有些人觉得更优雅。但说实话，在现在的项目里，PSL 已经很少见了。

PSL 的例子：

-- 同样的检查，用 PSL 写
property p_valid_data is
  always (valid -> next[1] data_valid);
end property

assert p_valid_data;

1.4 SVA 与 PSL 的对比

对比项	SVA	PSL
标准化	IEEE 1800（SystemVerilog）	IEEE 1850
语法风格	类 Verilog，容易上手	类数学逻辑，学习曲线陡
工具支持	所有主流仿真器都支持	支持较少，逐渐边缘化
我的推荐	强烈推荐，新项目首选	除非是维护老项目，否则别碰

1.5 断言的核心语法结构

不管是 SVA 还是 PSL，断言的核心结构都差不多。我画了一张图，帮你理清思路：

从这张图你可以看到，断言的结构是分层的：

• 最底层：布尔表达式（比如 a & b）和序列（比如 a ##1 b，表示 a 之后 1 个周期 b 成立）
• 中间层：property，把序列和表达式组合成完整的属性描述
• 最上层：断言语句，告诉工具这个 property 是用来 assert（检查）、assume（假设）还是 cover（覆盖）

1.6 断言的三兄弟：assert、assume、cover

SVA 里断言有三种类型，我管它们叫「三兄弟」：

• assert：大哥，负责检查。如果 property 不成立，就报错。这是最常用的。
• assume：二哥，负责约束。告诉仿真器或形式化工具，某些条件必须满足。在形式化验证里特别重要。
• cover：三弟，负责覆盖。检查某个 property 是否被触发过。用来衡量验证的完备性。

举个例子你就明白了：

// assert：检查 reset 后 10 个周期内 init_done 必须拉高
assert property (@(posedge clk) 
  $rose(reset) |-> ##[1:10] init_done);

// assume：假设输入信号 a 和 b 不会同时为高
assume property (@(posedge clk) 
  !(a && b));

// cover：记录 valid 拉高的事件
cover property (@(posedge clk) 
  $rose(valid));

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

最后分享一个我亲身经历的故事。有一次我负责验证一个 DDR 控制器，协议复杂得要命。刚开始我没写断言，全靠看波形。结果呢？一个 bug 藏了整整两周才被发现——因为那个 bug 只在特定时序下触发，波形上根本看不出来。

后来我花了三天时间，把协议里的关键时序要求都写成了断言。你猜怎么着？第二天就跑出来一个断言失败。定位后发现是一个状态机跳转条件写错了。从那以后，我每个项目的第一件事就是：写断言。先写断言，再写 testbench。这个习惯我一直保持到现在。

嗯，断言基础就讲到这里。记住一句话：断言不是锦上添花，而是雪中送炭。没有断言的验证，就像没有安全带的赛车——也许能跑，但风险太大了。