形式化验证器报告"已证明"，芯片却依然是坏的
我们自己的工具第一次对我撒谎时，它撒得很客气。形式化引擎返回了一个绿色对勾。我们要求它证明的每一条属性都返回了已证明。断言库看起来很完整。纸面上，这个设计已通过验证。
我们花了两天才意识到这份证书毫无价值——而且我此前对半导体 AI 验证的所有假设，都在防范一个错误的失效。
这些属性是由一个我们包裹在形式化引擎外面的大语言模型生成的——正是当时人人都在搭建的那种光鲜的 agentic AI 芯片设计演示。而引擎在几毫秒内就证明了它们，这本该是一个破绽。它们被证明了，因为会检验它们的那些条件从未触发。一条声称“每个请求最终都会得到授权”的属性，如果请求根本不可能发生，那它就平凡地为真。求解器并没有错。它回答了我们无意间提出的问题，而这个问题是空的。就在那一刻，我明白了这些 AI 验证流水线真正需要防范的是什么——以及为什么几乎没有一个卖这种东西的人在防范正确的目标。
我想告诉你我们的发现，因为那些扼杀现代芯片的缺陷类别，并不是业界宣传自己能捕捉的那些。我们为无晶圆厂芯片团队构建定制化的验证流水线——用微调过的开放权重模型包裹团队已经拥有的形式化引擎，完全运行在他们自己的硬件上——而这整套方法，正是从一开始把这件事做错中总结出来的。你可以在这里看到它的大致样子：veriprajna.com/solutions/semiconductor-ai-verification。但只有当你亲眼见过一个“通过”的设计失败之后，这套方法才会真正说得通。
一个应该吓到每一位无晶圆厂 CFO 的数字
有一个统计数据勾勒出了整个问题的轮廓。2024 年 Wilson Research Group / Siemens EDA 功能验证研究——业界历时最久的基准调研——将首次流片成功率定在了 14%。这是二十年跟踪记录中的最低值。2020 年，这个数字约为 32%。四年间，它下降了一半以上。
这并不是一个工程师变懒的故事。它讲的是复杂度跑赢了工具，以及规格说明的变异速度快过了追赶它的测试平台。同一项研究发现，大约 70% 的重新流片是由与规格变更相关的错误造成的——而非纯粹的逻辑缺陷。
首次流片成功率下降，并不是因为芯片团队变差了。它下降，是因为如今规格说明的变化速度，已经快过验证能够收敛它的速度。
我盯着那个 70% 的数字琢磨了很久，因为它悄悄地控诉了许多“面向芯片设计的 AI”的推销说辞。如果大多数重新流片都源于规格漂移，那么一个只能捕捉逻辑缺陷的工具，不过是在解决问题的一小块，却声称自己解决了整块蛋糕。
而出错的代价之残酷，是软件从业者所低估的。一套 5nm 掩模的成本高达 1000 万至 2000 万美元。到了 3nm，你就接近 4000 万美元，掩模层数超过七十层，其中包括二十多层 EUV 层。如今一次完整的 2nm 流片，成本大约在 7.25 亿美元这一量级，全部算上。一旦有问题漏了过去，重新流片意味着在掩模账单之上再叠加三到六个月的进度延误。在一个十八个月的产品窗口里，六个月的延误可能抹去一款芯片生命周期收入的一半。CFO 并不把验证看作一个成本中心。他们把它看作一份保险，防范一次八位数的错误。
大语言模型在硬件中究竟是如何产生幻觉的？
你的团队已经在用大语言模型处理 Verilog 了。我不会假装事实并非如此，向你推销的任何人也不该这么假装。如今这个研究领域是实打实的了——关于大语言模型编写 Verilog 的论文，从 2020 年的一篇增长到了 2025 年的六十四篇。在 VerilogEval 基准中较难的题目上，GPT-4 级别的模型能达到大约 43% 的功能正确率。有用。但不可信。
有意思的问题不在于这些模型是否有帮助。而在于它们如何失败，因为这些失败模式，看起来并不像软件工程师被训练去畏惧的那类失败。在无数个深夜盯着“看起来正确”的 RTL 为何出错之后，我开始把这些失败归为五类。
第一类是无害的那种。句法幻觉——就是那种根本无法编译的代码。Verilator 或综合前端会在几秒内捕捉到它。人人都已经知道该怎么处理这种情况，而这也正是人们想宣称问题已解决时所指向的那一类。
第二类，是开始造成伤害的地方。语义幻觉，教科书式的案例就是阻塞赋值与非阻塞赋值之争。一个在 Python 和 C 上训练出来的模型，会把 Verilog 当作语句自上而下顺序执行来读。于是它写下一个阻塞赋值——一个普通的 =——放在一个时钟驱动的 always_ff 块里，而这里语言要求的是非阻塞的 <=。设计者想要的是一个两级流水线。用阻塞赋值，第二级读到的是第一级的新值，而不是旧值，于是硅片交付出来的却是一个单周期旁路。某些仿真器会以一种完全掩盖这种竞争的顺序来调度事件。仿真起来没问题。综合出来的却是错误的机器。
第三类，是它教会我在第二块显示器上一直开着 AMBA 规格说明的那一类。协议幻觉。代码能编译，能通过九成的定向测试，然后却在从设备准备好接收地址之前，就置起了写数据有效信号——这违反了 AXI 握手协议。或者它把一个有效信号一直拉高，同时却在下面翻转数据。又或者它触发了埋在总线规格说明第 84 页、没有哪个人记得住的某条子条款。这颗芯片在你的内部测试平台上运行得完美无缺，可一旦接到第三方内存控制器上就会立刻挂死。你无法靠更多的仿真周期来蛮力解决它。你要靠针对每种协议编写的预验证断言库来捕捉它。
第四类，正是骗过了我们的那一类，也是危险的那一类。
为什么“已证明”是验证报告里最危险的一个词？
空洞幻觉。模型生成了一条 SystemVerilog 断言。形式化引擎证明了它。你就交付了。而这条属性之所以平凡地为真，是因为它的前件——那个“如果”的部分——从一开始就从未成立。
设想一条仲裁器属性：如果发起了一个请求，那么必须在若干周期内给出授权。现在假设同一个模型，出于“帮忙”的好意，还写了一条假设，强制把请求信号拉低。形式化引擎便尽职地在几毫秒内证明了这条授权属性，因为根本没有请求去违反它。底下真正的仲裁器也许已经彻底坏了。证书上写着“已证明”。它毫无价值。
一次在几毫秒内跑完的形式化证明，不是快。是可疑。引擎也许根本什么都没有证明。
这不是什么边缘风险。Siemens 从 2017 年起就一直在发布关于空洞证明的警告，而这个领域至今仍在交付没有自动空洞性检查的流程。当我告诉人们，一个没有空洞性检测的形式化验证流程，是更糟糕的——比完全不做形式化验证还要糟——他们就觉得我在小题大做。我没有。没有验证会让你恰如其分地感到害怕。而一句空洞的“已证明”，却让你既自信又错误，还带着一个已签核的模块奔向流片。这正是差点在我们自己早期原型中交付出去的那种失败，它永久地改变了我们所构建的东西。
第五类，是仿真在结构上根本无法看见的那一类。跨时钟域盲区。大语言模型读的是信号名；它感知不到时钟域。于是它把一个来自 2 GHz CPU 域的信号，直接连进一个 400 MHz 外设域的触发器，跳过了防止亚稳态的双触发器同步器。RTL 仿真并不对亚稳态建模——所以回归测试每一次都能通过，而硅片却在现场死锁。这就是为什么 CDC 缺陷会吞掉整套掩模。这也是为什么 Accellera 在 2024 年启动了一项 CDC/RDC 互操作性标准：商用 CDC 工具之间的碎片化，已经严重到足以让签核失效。
第二类到第五类，共有一个可怕的特性：它们都能通过仿真。它们只在硅片上才浮现。那正是至今仍会炸掉流片的那一类缺陷，也恰恰是一句“能捕捉逻辑缺陷”的推销说辞所遗漏在桌面上的那一类。
芯片团队真正面对的那堵供应商高墙
当我为一次流片去寻找真正独立的帮助时，我找到的选项比几年前还要少——这不是怀旧，而是市场结构使然。一位设计验证负责人真正能选择的三家 EDA 供应商——Synopsys、Cadence、Siemens——已经从十年前不到 75% 的市场份额，涨到了今天的超过 85%。再把 Synopsys 的 350 亿美元收购 Ansys 这笔交易算进去，前四家就掌控了大约 90%。一家无晶圆厂初创公司选购的市场，是收窄了，而不是拓宽了——恰恰是在问题变得更难的时候。
而且这些行业巨头在 AI 上也没有停下脚步。Synopsys 推出了 AgentEngineer，那是 2026 年 3 月发布的一套 agentic AI 验证工作流，号称能带来二到五倍的生产力，它构建在 VC Formal 之上——是我评估过的最可信的供应商 agentic 技术栈。Cadence 则宣布了它的 ChipStack AI Super Agent，那是 2026 年 2 月的事，并用 Cerebrus AI Studio 来做强化学习驱动的实现，而 JasperGold 依旧是那个作为黄金标准、别人都拿来作衡量基准的形式化引擎。我这话说得毫不含糊：JasperGold 和 VC Formal 是真正出色的。任何一上来就贬低它们的人，都等于告诉了你，他们从没真正完成过一次流片。
问题出在价格和姿态上。JasperGold 的历史基准价格大约在 22.5 万美元，外加每个席位 4.5 万美元——对一家大型无晶圆厂公司来说没问题，但对那些正在做着最有意思工作的早期 RISC-V 和 AI 加速器初创公司来说，就遥不可及了。而且这些巨头最新的 AI 功能都是云优先的，这与这些客户绝不肯让步的那一条要求正面相撞。这一点稍后再说。
接下来是那股初创浪潮，而且声势浩大。在最近一届 DAC 和 DVCon 上，我合作的一位 DV 负责人，一个季度里就被八家不同的“面向芯片设计的 agentic AI”公司推销过。ChipAgents 截至 2026 年初已融资 7400 万美元，并宣称能带来十倍的设计与验证生产力。Normal Computing 在三星 Catalyst Fund 的领投下融资 5000 万美元，做的是自动形式化——让大语言模型把工程师的意图直接翻译成形式化属性并加以证明——并声称全球排名前十的半导体设计公司里有一半正在使用它。还有更多：MooresLabAI 生成完整的测试平台，Bronco 做回归分析，Silimate 做功耗-性能-面积预测。
其中有些是真材实料。但没有一家解决了客户真正的问题，那就是：他们如今买了三款这样的单点工具，却完全不知道该如何让它们在自己早已信任的签核流程里协同工作。
那个没人愿意公开说出口的强化学习布局故事
在芯片设计中，除了验证之外还有一个与之并行的诱惑：用强化学习来做物理平面规划——决定那些大模块在晶粒上摆在哪里。它很诱人，而被引用最多的那个成果，正以一种大多数推销说辞恰好略过的方式受到质疑。
2020 年 Google 发表在《自然》上的那篇论文声称，在宏单元布局上强化学习胜过模拟退火，而且它已被用在真实的硅片上——好几代 TPU 都搭载了它。但在 2023 年，在有人提出方法学上的疑虑之后，《自然》加了一条编者按。如今在 Synopsys 任职的 Igor Markov，发表了一份逐行的批评，其中最醒目的一项对比让人过目难忘：强化学习方法耗时 32.31 小时，一个调优过的模拟退火基准耗时 12.5 小时，而一款商用的 Cadence 工具完成同样的工作只用了 0.05 小时。DeepMind 则以一篇题为“That Chip Has Sailed”的论文予以回击。多年过去，没有任何独立的外部复现能证实最初的那些声称，而这份批评和这份反驳至今都仍未了结。
我提这件事，是因为当一位顾问向一支真正搞形式化的团队推销强化学习布局，还假装这场争议根本不存在时，会发生什么。他们十分钟之内就能嗅出破绽，而你也就失去了整个会场。诚实的立场是：确实存在一些真正的利基领域——芯粒与 3D-IC 的热感知平面规划、模拟版图、在开源工具链上的 RISC-V IP 优化——在那里，混合方法能够物有所值。而对巨头们的布局引擎发起正面强攻，则不能。懂得这其中的区别，并把它公开说出来，才是这份工作的全部。
我们的工具骗过我们之后，改变了什么
于是，那场空洞证明的灾难把我们引到了这里。我们不再试图去打造一个更会写 Verilog 的 AI，因为那是一条挤满了八位拿到融资选手的赛道，而是开始构建他们谁都不卖的那样东西：供应商中立的集成层，让一支团队现有的工具变得可信。
具体来说，这意味着几个决定，每一个都是被我们亲眼见过的某次失败逼出来的。我们在客户自己的 RTL 语料库、他们的规格说明、他们过去的缺陷历史上，微调一个开放权重模型——Qwen Coder、Llama，哪个合适用哪个——因为一个没见过你家代码风格的模型，会针对它产生幻觉。我们把它包裹在团队已经拥有的任何一款形式化引擎外面：JasperGold、VC Formal、Questa Formal，或者开源的 SymbiYosys。我们从不要求他们拆掉自己早已信任的那款黄金标准工具。而模型提出的每一条属性，都必须先经过空洞性与覆盖率检查，才允许任何人读到“已证明”这个词——因为我们以昂贵的代价懂得了，一个不设防的证明不过是一场表演。
预验证的断言库，和模型同样重要。对于一个 RISC-V 核，形式化测试框架自带 AXI4、AHB 和 TileLink 的合规性检查、流水线冒险断言、加载-存储记分板、调试单元正确性属性——这些正是能在硅片之前就捕捉到协议幻觉和语义幻觉的东西。这并非空谈。形式化验证咨询公司 Axiomise 已经发现了 Ibex 中的 65 个以上缺陷——Ibex 是 Google OpenTitan 内部的那个开源 RISC-V 核——其中包括调试单元里只有形式化方法才能捕捉到的分支指令缺陷。形式化方法在 RISC-V 上是奏效的。稀缺的不是方法本身；而是一支懂得如何驾驭它的团队。
这里真正的机会，从来都不是一个更聪明的 Verilog 模型。而是一套诚实的测试框架，包裹在一支团队早已信任的那些昂贵工具外面。
你为什么不干脆把它跑在云上？
人们不停地问我这个问题，而答案，正是每一家云优先的 EDA-AI 初创公司，在我所在意的那些客户面前一到场就注定出局的原因：RTL 是皇冠上的明珠，它绝不离开这栋大楼。
一家无晶圆厂公司的寄存器传输级代码就是这家公司。国防和航空航天客户需要它物理隔离，有时还要放在一个保密设施里。商用无晶圆厂团队则要求本地部署，最低限度也得是虚拟私有云。所以我们把一切都跑在客户自己的硬件上——在他们现有的 H100 或 H200 集群上用 vLLM 或类似方案做推理，在他们自己的语料库上做本地检索，任何 RTL 永远都不越过网络边界。巨头们最新的 agentic AI 功能都是云优先的；那对他们是卖点，对一支对 IP 敏感的芯片团队却是根本无法接受的。我所看到的最大机会，压根就不是一个算法问题。它是一个部署与集成的问题，而那些拥有最好算法的人，已经决定不去解决它。
另一个问题来自汽车团队，而它对他们来说是决定一切的那个问题。要把一颗芯片送进达到 ASIL C 或 D 等级的汽车——在这些安全完整性等级上，ISO 26262 不再只是建议做形式化验证，而是开始强制要求——那么工具本身就必须带有 TCL2 或 TCL3 资质认证包。巨头们的核心引擎拥有那种第三方认证；而一款全新的 AI 工具没有。我曾亲眼看着一款确实更出色的工具，正因为这个原因在某个汽车项目里被搁置：没有资质认证包，就没有在签核流程里的位置，谈话到此结束。所以我们并不试图去成为那款合格的工具。我们帮助团队，让 AI 辅助与那些合格的巨头引擎并肩运行，同时又不破坏资质认证链——因为在汽车领域，一款在技术上更优越、却无法经受住审计的工具，一文不值。
证书不是芯片
我一次又一次地回想起那两天，我们把信任交给了一个毫无意义的绿色对勾。教训并不是“大语言模型不擅长 Verilog”。它们每个季度都在变得更好。教训在于，在硬件里，看起来已验证与确实已验证之间的鸿沟，是以八位数的掩模和六个月的延误来度量的——而争相涌入这一领域的工具，大多只是在赛着把“看起来已验证”这部分做得更快。
在一套 1000 万美元的掩模上，一句你无法追溯到某个非空洞证明的“已证明”、跑在你所掌控的硬件上、针对由某个读过规格说明第 84 页的人所编写的断言——那不是验证。那是一份制作精良的空想。如果你想看看我们是怎么分辨这种区别的，一切都摆在这里：veriprajna.com/solutions/semiconductor-ai-verification。
芯片并不在乎报告说了什么。它只做硅片实际被造出来去做的事。验证，就是让这两件事变得一致的那门功夫——而当一个 AI 在几毫秒内告诉你它们是一致的那一刻，恰恰就是你该去把规格说明拿到手里的时候。
