6.3 形式化验证：数学证明代替穷举

6.3 形式化验证：数学证明代替穷举

本节摘要：形式化验证不跑任何具体激励，而是把"电路在所有输入下都满足某性质"变成一个数学命题，交给 SAT 求解器或模型检查算法去证明或反证。本节从布尔可满足性问题讲到 CDCL 求解器的机制，拆解等价性检查（综合签核的守护者）与模型检查（协议与安全属性的证明者）两类应用，并直面状态爆炸这头房间里的大象。SVG 图展示 SAT 求解一个电路性质判断的完整过程。

换一个提问方式：从"跑过没问题"到"证明没问题"

仿真的完备性天花板在第 6 章导语里已经算过：一组激励没发现问题，不等于问题不存在。形式化验证换了提问方式：把设计 M 与性质 P 交给数学，回答"M 满足 P"是真还是假——真则给出全部输入空间的保证，假则通常附赠一条反例（让性质失效的具体输入序列）。这个转换的秘密武器是把问题编码成布尔可满足性（SAT）：给定一个布尔公式，问存在让它为真的变量赋值吗。电路与性质都能机械地翻译成 CNF 公式（合取范式）：电路的每个门产生若干子句，"性质不成立"的约束再编码进去——公式可满足等价于存在反例，不可满足等价于性质成立。一步跨越从"枚举不完"到"一次求解判全体"。

SAT 的搜索空间名义上是 2 的 n 次方（n 为变量数），但现代求解器远比穷举聪明。DPLL 框架（1960 年代）的两件事是根基：单元传播——某子句只剩一个未赋值变量时，该变量的取值被强制（立即传播，大量变量无需猜测）；纯文字消除与早期剪枝。**CDCL（冲突驱动子句学习，1990 年代末）**是工业突破：搜索走深遇到冲突（某个赋值组合使子句全假）时，分析冲突的"原因变量集"，生成一个学习子句（记录这次冲突的教训）加入公式，然后回跳到原因层——而不是笨拙地回退一步。学习子句让求解器"吃过一次亏就永远记得"，配合 VSIDS 决策启发（按参与冲突的频度选变量），实际工业实例的求解能力比朴素穷举高出二十多个数量级——这是算法工程史上最戏剧性的实用化跃迁之一， 也是形式化方法在 2000 年代从学术走向工业的直接原因。

图：SAT 求解如何宣判一个电路性质

等价性检查：综合签核的守护者

形式化验证在 EDA 流程里最重量的应用是等价性检查（EC）：证明综合或重构前后的两个电路功能完全相同。2.3 节已经预告过它的角色：综合引擎的优化变换大胆激进，等价性检查在事后逐点验证——两个电路的对应输入并在一起、对应输出做同或、公式的 UNSAT 即等价。直接对整图证明会大得离谱，工业 EC 的关键技巧是映射点分割：综合器在每次变换时记录前后对应关系（寄存器边界、可证明等价的中间节点），检查被切成一串小规模子问题，每个子问题一个 SAT 调用——"增量证明"让整体难题分解为十万个小题，每题毫秒到秒级。跨综合的时序等价（带时序约束的功能等价）与安全属性的检查也在同一框架上扩展。

模型检查：证明"行为协议"而非"一次快照"

等价性检查证明的是"两个电路相同"，模型检查（MC）证明的是"一个电路的所有行为满足某时序性质"——性质用时序逻辑书写（LTL/CTL）：例如"仲裁器的授权请求最终都会被响应"、"锁定信号有效后地址不会再变"。工业主流算法是有界模型检查（BMC）：把时序电路在时间上展开 k 拍，"k 拍内存在违反性质的轨迹"编码成 SAT——可满足即给出反例轨迹（真金白银的调试输入），不可满足证明 k 拍内无反例。配合不动点判定（反例长度超过状态空间直径即不存在），BMC 与交互加深构成完备证明。它的克星是状态爆炸：数据通路类设计（宽位加法器、乘法器）状态空间天文数字，模型检查往往超时——这就是三出口图里"出口三"的现实来源。工业对策：抽象化（把不相关的宽总线抽象成小状态）、属性分解（把大性质拆成局部小性质）、以及把形式化用在它擅长的地方——控制逻辑、仲裁器、协议接口、安全关键属性，而不是硬啃乘法器。

验证计划里的排兵布阵

把本章三节排进一张作战图：仿真铺量——约束随机激励加功能覆盖率高产出的"跑量"验证；形式化钉点——对控制密集、属性清晰的模块出数学证明，对仿真覆盖率长期到不了的黑洞出反例；等价性检查守流程——综合、重构、ECO 每次变换后的等价背书，这是 EDA 流程里唯一由机器自动全程执行的形式化应用。覆盖率的账本两本并读：仿真覆盖率说"跑过的输入空间占多少"，形式化的证明清单说"哪些性质已全覆盖"——两本账合并核算，才是现代验证计划的完整语法。至此，本书的技术主线（综合、物理实现、签核、制造协同、验证）全部走完，第 7 章看 AI 如何在这条主线的每一环上动土。

SAT 求解器的进化速度可以用一个公开事实感受：国际 SAT 竞赛（SAT Competition）逐年更换冠军实现，工业实例的求解能力十年间提升多个数量级，衍生工具链（SMT 求解器、约束求解内核）也随之换代。EDA 工具普遍把求解器做成可插拔组件，引擎层迭代不惊动上层应用——这与第 8 章要讲的"脚本与引擎松耦合"是同一个工程哲学。对使用者而言，务实的一句话是：不要在自己的代码里硬编码求解器的行为细节，把它当黑盒服务调用。

再补一个关于"证明代价"的工程事实：形式化验证的人力成本主要不在跑求解器，而在写性质。把"仲裁公平"这类模糊需求翻译成精确的时序逻辑性质，需要同时懂协议语义与时序逻辑语法的人，性质写错（过强则大量假违例、过弱则证明失去意义）的返工是这类项目的主要开销。成熟做法是建立性质库：同类的仲裁器、FIFO、握手协议各有一组经过审阅的标准性质模板，新设计填参数复用——性质资产化与第 8 章的脚本资产化是同一个思想在验证域的投影。

本节要点回顾

• 换提问方式：把"跑过没问题"升级为"证明全空间没问题"，SAT 是转换的枢纽。
• CDCL 的实用奇迹：传播、冲突分析、学习子句、回跳，比穷举高二十多个数量级。
• 三出口纪律：UNSAT 性质成立、SAT 给反例、超时只给未知——未知不等于通过。
• 等价性检查：映射点把整图难题切成小题，是流程中全自动的形式化应用。
• 模型检查的阵地选择：控制逻辑与协议属性是主场，数据通路的宽位运算易状态爆炸。
• 双保险语法：仿真铺量、形式化钉点、EC 守流程，两本覆盖率账合并核算。