为什么在 AI4EDA 里仍要坚持形式化方法

动机

近年 AI4EDA 把图神经网络、强化学习甚至大模型塞进布局、布线、逻辑综合与验证流程，吞吐和探索效率明显上升。可一旦模型输出进入硅前关键路径，一个沉默的错误会比一次慢搜索更贵。

本文想说清楚一件事：加速探索与保证正确是两类问题；形式化方法不是 AI 的对立面，而是把模型产出关进可检查笼子的手段。

三条分工

1. 模型负责提议：候选变换、候选不变量、候选切割点、候选测试激励。
2. 形式化引擎负责裁决：等价性检查、模型检测、SMT/SAT、定理证明器给出 yes/no/unknown。
3. 综合与实现负责落地：在已验证的约束下做技术映射与优化。

把「生成」和「判定」拆开，流水线才能既快又敢合入。

一个小例子：学习引导的等价性检查

假设有两个 RTL 版本 A（参考）与 B（经 AI 建议的逻辑重写）。流程可以是：

1. 模型根据数据流图提出一组候选 cut-point / 中间等价点。
2. 用商业或开源 equivalence checker 在这些点上做局部证明。
3. 失败时把反例反馈给模型，缩小下一轮搜索空间。

关键点不在「模型是否聪明」，而在最终合入条件必须是 checker 通过，而不是置信度分数。

和定理证明的衔接

对协议级属性、总线一致性、部分算术数据通路，bounded model checking 不够时，可以把核心引理搬进 Lean / Coq / Isabelle。AI 适合草拟证明脚本；人类与 kernel 负责验收。站点笔记区会陆续放这类草稿（见 /notes）。

实践清单

• 任何 AI 改写的 RTL：至少跑一遍等价性或属性检查再进综合。
• 把「未知 / timeout」当成一等公民，不要用启发式「看起来像对」填坑。
• 记录假设（时钟、复位、X 传播、不等价的 don’t-care）——假设漏写等于证明无效。

小结

AI4EDA 改变的是搜索曲线；形式化验证与定理证明改变的是可接受集合的边界。个人站后续博客会围绕「学习提议 + 形式化裁决」写更多工具链笔记。

← 返回 Blog