形式验证（formal verification）
想象你造了一把数字锁，你想确认：没有正确的密码，它绝不可能打开。用仿真，你会输入几千个错误密码，每次都看着它保持锁闭，于是感觉挺踏实——但你只检查了恰好试过的那些密码。形式验证走的是相反的路：它不去测试若干例子，而是用数学证明——证明任何可能的输入、以任何顺序，都绝不可能把这把锁打开。一份滴水不漏的证明，顶得上无穷多次试验。
具体来说，形式工具会接收你的设计（即 RTL）外加一条你写下的属性——一句精确的断言，比如「授权信号绝不会同时对两个主设备置位」——并把整个电路当作一个数学结构，对它全部可达的状态空间进行推理。如果该属性在每一种合法的输入序列下都成立，工具就返回已证明。如果不成立，工具会交给你一个具体的反例：一段精确的波形，逐步展示是什么破坏了它。你再也不必为「测试写够了没？」而焦虑，因为这种搜索从构造上就是穷尽式的。这也使它成为断言的天然搭档——断言正是你用来陈述这些属性的语法结构，通常以 SystemVerilog 断言（SVA）写成。
玄机就藏在「穷尽」这个词里。它只对你陈述的那条属性、以及你所指向的那个设计模块成立——形式验证完整地证明了那条主张，却并不证明你的芯片整体正确。而且可达状态空间会爆炸式增长，因此较大的模块可能撑爆内存或时间上限，迫使你去约束输入、分解问题，或者接受一个只在 N 个时钟周期内成立的有界证明。形式验证在控制逻辑、仲裁器和协议检查上锋利无比；但它不适合用来验证一个宽位的数据通路乘法器，那种场合约束随机仿真仍然大有用武之地。
// At every clock edge (outside reset), at most one grant is asserted.
property p_grant_mutex;
@(posedge clk) disable iff (rst)
$onehot0(grant);
endproperty
a_grant_mutex: assert property (p_grant_mutex);上面那条「两个主设备」属性，写成一条厂商中立的 SystemVerilog 并发断言，表达的是 grant 至多是独热（one-hot）的——在任意时钟下至多有一位被置位。形式工具要么返回已证明——任何可达状态都不会同时拉高两个 grant——要么给出一段反例波形，精确展示两个主设备是如何同时被授权的。
「形式验证」和「模型检验」常被当作同义词混用，但模型检验其实只是形式验证大伞下的一种技术（与等价性检验、定理证明并列）。它们共同的内核是：保证来自对所有情形的数学证明，而不是来自跑几个例子。