你距离 Formal Verification 的 offer 到底有多远

聊聊 Formal Verification：一个被严重低估的芯片验证方向

芯片验证（DV）这个圈子里，大家默认聊的都是 functional verification——写 testbench、跑 UVM、看波形、追 coverage。但还有一个方向，很多人听说过名字，却从来没认真了解过：Formal Verification（形式化验证）。这篇帖子就来聊聊 formal 到底是什么、日常工作在做什么，以及为什么它变成了一个越来越火的方向。

什么是 Formal Verification

functional verification 是"跑出来看对不对"，formal verification 是"证明出来一定对不对"。
传统的 functional verification，本质上是仿真（simulation）。你写一堆 testbench、randomize 一堆输入、跑成千上万个 test case，然后看 DUT（Design Under Test）的行为对不对。这套方法的局限很明显：你永远只能验证你想到的场景。设计里藏得比较深的 corner case，如果你的 testbench 没有恰好触发到，它就永远不会被发现——直到芯片流片之后才会被发现。
Formal verification 走的是完全不同的路子。它不跑仿真，而是用数学的方法（基于 SAT/BDD 等求解器），针对你写的 property（属性，也就是设计应该满足的行为约束），对设计的所有可能状态空间做穷举式的证明。简单说：

• Functional verification：跑一亿个随机场景，覆盖率 99%，剩下 1% 可能有 bug 但你不知道。
• Formal verification：数学上证明，在所有可能的状态下，这条 property 都成立（或者找到一个具体的反例，告诉你哪里会挂）。

这也是为什么 formal 在验证一些复杂的控制逻辑（比如仲裁器、总线协议、cache coherence 状态机）时特别有价值——这类模块的状态空间巨大，光靠随机仿真很难覆盖干净，但用 formal 可以做到"证明它不会出错"，而不是"跑了很多次没出错"。

Formal DV 工程师平时在做什么

日常工作大致可以拆成这几块：

• 写 SVA property：把设计规格（spec）转化成 SystemVerilog Assertions，描述设计"应该"满足的行为——比如握手协议不能死锁、仲裁一定公平、某个状态机不会进入非法状态。
• 搭建 formal 环境：配置 formal tool（业界主流是 Cadence 的 JasperGold，也有 Synopsys VC Formal 等），把 property、assumption、约束这些接入到工具里。
• 跑 property check，分析结果：工具会给出三种结果——proven（证明成立）、falsified（找到反例，说明有 bug）、inconclusive（状态空间太大，没跑完/需要抽象化处理）。大量的日常工作其实是在分析 inconclusive 的结果，想办法通过抽象化（abstraction）、black-box 部分模块等手段让证明收敛。
• Bug 复现与 debug：formal 工具找到反例之后，会给出一条具体的 waveform，说明"在这个输入序列下，property 会被违反"，工程师需要据此定位设计问题。
• 和 RTL 团队配合：formal 往往会比 functional 更早介入设计阶段，因为它不需要一个完整可跑的 testbench，只要有 RTL 就可以开始写 property，这也是它在很多公司里被用作"设计早期质量把关"手段的原因。

为什么大家都不投 formal 的岗位？

聊完了 formal 是什么、日常做什么，回到一个更现实的问题：既然 formal 这么有价值，为什么找工作的时候愿意投这个方向的人反而很少？
核心问题是信息差。Functional verification 还好，网上视频、书籍、资料到处都是，随便搜都能找到一条学习路径。但 formal verification 呢？你会发现 GitHub 上连一个完整、系统的学习仓库都几乎没有。很多同学找工作的时候，对 formal 的概念是什么、面试考什么、岗位要求什么，完全没有概念，于是就自动把这些岗位归到了"和我无关"的那一类，直接跳过。
但这个信息差，恰恰就是机会所在。
随着 AI 的发展，formal verification 的很多传统瓶颈正在被逐步解决，市场上对 formal DV 工程师的需求在明显增加。而且 formal 在实际工作中很大程度上是工具驱动的——用 JasperGold 跑 property check，写 assertion，分析结果，都是具体的工具操作。问题在于，工具的使用经验很难在面试里直接考察。面试官没办法让你当场跑一个工具，只能聊思路聊概念，这就导致 formal DV 的面试难度比 functional DV 低了不少。
面试官对 formal 候选人的预期本来就更宽松。他们也清楚这个方向学习资源少，愿意主动来了解的人本身就不多。你如果做过哪怕一个 formal 的小 project，已经超过了很多候选人；如果你对 JasperGold 这样的工具有过实际应用，那基本上已经把一大批竞争者挤出去了。
逻辑就是这样：大家都以为 formal 很难入门，于是都不投；越没人投，竞争压力就越小；竞争越小，你拿到 offer 的概率就越高。formal 方向整体拿 offer 的效率明显高于 functional 方向，这不是偶然。

写在最后

如果你目前正在准备 DV 方向的求职，不妨认真考虑一下把 formal 也纳入准备范围。它不需要你抛弃已经在学的 SystemVerilog 和 UVM 基础——恰恰相反，SVA 本身就是 formal 的核心语言之一，你在 functional verification 里学的 property 写法，可以直接迁移过来。真正需要补的，是 formal 特有的思维方式（怎么写出可以收敛的 property、怎么做抽象化）和工具经验（哪怕只是找一个开源设计，用 JasperGold 或者免费版工具跑一跑）。
这条路目前确实资料少、入门门槛看起来高，但正因为这样，先动手的人反而更容易占到先机。
而且因为以上的原因，所以面试官对面试人的期待就会大幅度降低，很类似五六年前的 functional verificaiton 岗位，当时会 UVM 的毕业生寥寥无几，如果你在当时可以写 UVM 就是一个很大的优势，现在也类似，即使你只会用 formal 来验证一个简单的 fifo，也足够和其他同学拉开巨大的差距，更何况我们课上讲了七种 formal 的验证实战方法以及 6 个应用的 project，足以帮你建立起足够的优势。
最后，真的学了 formal 的知识也不一定真的要去面试 formal 的岗位，现在很多的 functional verification 的岗位招聘下面几乎都会写 formal experience is a plus, 所以多一项别人不会的知识，你就多了一点拿到 offer的可能。

更多北美芯片求职信息，欢迎加入同芯同行社区：https://tongxintongxing.com

这个和Lean还有TLA+什么关系？

我之前写了很多coq，但是方向主要是做到密码学里面去了。投硬件公司的formal职位没有回应，crypto的有些但也不是很多…楼主大大可以帮推荐一下嘛

匿名用户 发表于 2026-09-14 17:34:03
这个和Lean还有TLA+什么关系？

tla+是指导分布式设计的，lean和coq一样，是证明的验证。硬件据我所知用的大多还是model checking