AI 写出的那个 1000 万美元 bug——以及我为什么创办一家公司要消灭它
我清楚地记得自己决定创办 Veriprajna 的那一刻。
那不是一次灵感的迸发。那是一通电话。就是那种在最初五秒钟里无人开口的电话，因为电话另一端的人正努力思考该如何说出他要说的话。一个设计团队——都是我尊敬的人，是真正擅长本职工作的人——刚刚从晶圆厂拿回了一款定制 RISC-V 加速器的首批硅片。芯片报废了。不是那种“需要变通方案”的报废。不是那种“可以用固件打补丁”的报废。彻底变砖。在热降频与高带宽内存流量的一种特定而罕见的组合条件下，仲裁模块进入了未定义状态，整个系统随之死锁。
根本原因是一个竞态条件。RTL 中阻塞赋值与非阻塞赋值之间一处细微的单点不匹配——那种在仿真中完美运行、在 lint 检查中悄无声息、能通过你抛给它的每一项回归测试，然后在没有第二次机会的硅片上背叛你的东西。
那款 5nm 芯片的光罩组价格约为 1000 万美元。全没了。但真正的损失并不是光罩。而是诊断、修复、重新验证和重新流片所需的六个月。在 AI 加速器市场，产品换代周期约为 18 个月，六个月的延误就可能侵蚀掉一款产品整个生命周期毛利润的 50%。对于一家目标营收 1 亿美元的公司而言，那个竞态条件的代价并不是 1000 万美元。而是 5000 万美元。
而让我夜不能寐的正是这一部分：导致它的代码是由一个 LLM 生成的。
无人质疑的淘金热
眼下，半导体行业正处在一场淘金热之中。所有人——我是说所有人——都在争相把大语言模型接入电子设计自动化（EDA）流程。这个说辞令人无法抗拒：把过去动辄数年的设计周期压缩到数月。让芯片设计变得人人可及。让 AI 处理繁琐的寄存器传输级编码，好让工程师专注于架构。
我理解这种吸引力。我自己也曾感受过。当我第一次看到一个 LLM 从自然语言提示词生成出语法正确的 Verilog 模块时，我心想：这将改变一切。
但随后我开始更仔细地审视，当你写的是硬件而非软件时，“语法正确”究竟意味着什么。于是我意识到，这个行业是建立在流沙之上的。
眼下涌入市场的这些工具，就是我所说的“套壳工具”。它们拿一个通用 LLM——GPT-4、Claude、Llama——用一个带有 Verilog 风格系统提示词的聊天界面把它包裹起来，然后当作“芯片设计副驾”来兜售。其中有些确实是令人印象深刻的演示。代码看起来很干净。能编译。甚至能仿真。
但这些工具的本质是这样的：披着硬件外皮的随机词元预测器。它们不理解电路拓扑。它们不理解时序收敛。它们不理解亚稳态。它们只是根据训练数据中的统计模式预测下一个可能的词元。
当 LLM 在软件中产生幻觉时，你得到的是一个可以通过空中升级来修补的运行时错误。当 LLM 在硬件中产生幻觉时，你得到的是一块价值 1000 万美元的镇纸。
这种不对称正是 Veriprajna 存在的全部理由。
为什么 AI 会写出糟糕的硬件代码？
这是我被问到最多的问题，通常来自那些见过 LLM 写出完全可用的 Python、却无法理解 Verilog 为何不同的软件工程师。答案比“硬件更难”要深刻得多。这是 LLM 思考方式与硬件运作方式之间的一种根本性错配。
LLM 的训练数据绝大多数是软件——Python、Java、C++、JavaScript。这些都是命令式、顺序执行的语言。A 行执行，然后 B 行执行。系统的状态由操作的先后顺序决定。LLM 对这一范式的内化如此之深，以至于它基本上成了它们的母语。
Verilog 和 VHDL 则是声明式且并发的。在一个硬件模块中，每一个always块、每一条assign语句、每一次模块实例化都是同时且持续地执行的。源代码中各行的顺序，往往对硅片中执行的顺序毫无影响。
在我们早期的一次实验中，我实时目睹了这一幕的上演。我们让三个不同的前沿 LLM 实现一个简单的三级流水线寄存器。三个都用了阻塞赋值（=）而不是非阻塞赋值（<=）。如果你像看 C 代码那样眯着眼睛看，这些代码看起来完全合理。但在硬件中，时钟块里的阻塞赋值意味着stage2会立即被更新为stage1的值，然后stage3又会拿到stage2的新值——实际上把一个两周期的流水线坍缩成了一个周期。
我的一位工程师 Priya 盯着输出看了一分钟，说：“它是在把分号写错位置地写 C 代码。”她说得一点没错。这个 LLM 有顺序性偏见——它把 Verilog 当成一门编程语言来对待，而它实际上是一门描述语言。这种区别在语法上很微妙，在物理上却是灾难性的。
而且情况会更糟。硬件设计依赖严格的接口协议——AXI、AHB、PCIe、TileLink——它们有着复杂的时序规则。“Ready 不得等待 Valid。”“Grant 必须在 5 个周期内被断言。”LLM 生成的代码可以在 90% 的情况下遵守这些规则，这听起来很棒，直到你意识到它出错的那 10% 恰恰是那些会让芯片报废的边角情况。一个在特定子条款违规下先断言WVALID再断言AWREADY的 AXI 主设备不会抛出语法错误。它会编译、会仿真，然后在硅片上与一个合规的内存控制器相连时挂起。
训练数据的问题让一切雪上加霜。可用于训练的高质量、生产级 Verilog 的数量比 Python 或 JavaScript 小上好几个数量级。GitHub 上大量的开源 Verilog 是学生项目、被弃置的原型、以及那些永远通不过流片评审的玩具级实现。当你用平庸的数据训练时，你就会得到平庸的输出——看起来很专业，却携带着业余错误的 DNA。
困扰每一位芯片设计者的法则
半导体设计中有一条被称为“十倍法则”的经验法则，一旦你理解了它，你就会明白我为什么如此执着于尽早捕获 bug。
在设计生命周期的每一个后续阶段，修复一个缺陷的成本都会增加10 倍。在 RTL 设计阶段捕获的 bug，修复成本约为 100 美元——有人编辑一个文件并重新跑一次检查。同一个 bug 若在块级验证阶段被捕获，成本为 1000 美元。在系统验证阶段是 10000 美元。如果它逃逸到硅后验证——当你在实验室里调试真实芯片时——那么一次重新流片你要面对的是 1000 万美元甚至更多。而如果它抵达了现场的客户手中呢？那就是 1 亿美元的量级了。召回、诉讼、品牌毁灭。去问问英特尔关于奔腾 FDIV bug 的事吧。
这些套壳 AI 工具几乎只在 RTL 设计阶段工作。它们帮工程师更快地写代码。但由于它们除了“能不能编译”之外不具备任何验证能力，它们注入的 bug 会一路顺畅地通过块级验证和系统验证，最终在硅片上引爆。
而这里有一个残酷的讽刺：通过在不提升验证严格性的前提下提升代码生成的速度，这些工具反而加速了高成本缺陷注入流程的过程。你不只是在快速前进并打破东西。你是在快速前进，并把 bug 烘焙进价值 1000 万美元的光罩组里。
行业数据印证了这一点。只有 32% 的设计能实现首硅成功。其余 68% 至少需要一次重新流片，而首要原因是逻辑和功能缺陷——恰恰是 LLM 在产生协议幻觉或误解并发时会生成的那类错误。
我曾在融资早期向一位投资人解释过这一点。他耐心地听完，然后说：“你就不能用 GPT-4 配上更好的提示词吗？”
我调出了那个流水线寄存器的例子。我给他看了那个阻塞赋值的 bug。我给他看它如何通过了 lint 检查、通过了仿真、通过了套壳工具所提供的每一项自动化检查。然后我给他看了它在硅片上会造成什么后果。
他再也没有问过更好的提示词的事。
如果你能证明代码正确，而不只是测试它，会怎样？
故事在这里迎来转折。因为解决 LLM 幻觉问题的答案，不是更好的提示词、更大的模型，或更多的训练数据。而是一种根本不同的验证方法。
传统验证依赖仿真——你编写测试平台，运行数百万个周期，并检查设计是否如你所愿地工作。这就像通过绕着街区开上一千圈来测试一辆车的刹车。如果刹车没坏，你就假定它是安全的。但如果它只在下雨、你时速恰好为 62 英里、且收音机调到某个特定频率时才失灵呢？仿真只能验证它明确测试过的场景。其余的一切都只能靠祈祷。
形式化验证则根本不运行设计。它把整个设计转换成一个数学公式，并使用可满足性模理论（SMT）求解器——诸如微软的 Z3 之类的工具——来穷尽地证明某个属性在每一种可能的输入组合和内部状态下都成立。每一种都不例外。不是抽样。不是统计近似。而是一个数学证明。
仿真问的是：“在我测试过的这些情况里，它能工作吗？”形式化验证问的是：“是否存在任何一种可能让它失败的情况？”这个区别，就是希望与证明之间的区别。
当求解器返回“UNSAT”——不可满足——时，这意味着不存在反例。该属性在数学上得到了保证。当它返回“SAT”时，它会交给你一段能击垮你设计的具体输入序列，精确到确切的时钟周期。
形式化验证已经存在了数十年。它之所以没有席卷整个行业，是因为编写形式化属性——SystemVerilog 断言，即 SVA——出了名地困难。它需要一套大多数设计团队并不具备的专业技能。这些断言就是硬件的“契约”：“若 request 拉高，grant 必须在 N 个周期内跟上。”“从地址 X 读出的数据必须与最后一次写入地址 X 的数据一致。”“流水线绝不能死锁。”正确地编写这些断言是一门艺术，而能做这件事的从业者远远不够。
而这恰恰正是 AI 变得有用的地方——不是用来写硬件代码，而是用来写证明。
“形式化三明治”——我们究竟是如何构建它的
我花了好几个月与团队争论正确的架构应该是什么样。那场辩论很激烈，而如今回想起来，它厘清了很多东西。一派主张对一个 LLM 进行微调，直到它默认就能生成正确的 Verilog。另一派——我最终站到了这一边——则主张“靠训练获得正确性”是一种幻想。你无法把幻觉训练掉。你只能捕获它。
我们最终落定在我们称之为“形式化三明治”的方案上——一种神经符号架构，其中 LLM 是富有创造力的引擎，而形式化验证求解器则是毫不妥协的评判者。二者都无法独自运作。合在一起，它们能做到任何一方独立都做不到的事。
它在实践中是这样运作的。一位设计者提供一份规格说明——“设计一个 APB 到 AXI 的桥接器”，甚至是一张时序图截图。我们的规格分析智能体把它分解为一系列功能需求。接下来是关键创新：LLM 不只生成代码，而是同时生成两件产物。
产物 A是 RTL 实现——Verilog 代码本身。产物 B是形式化规格——一组从同一批需求推导出来的 SVA 属性。如果规格说“Grant 必须跟随 Request”，那么 LLM 既生成状态机，又生成证明该状态机确实如其所声称那样运作的断言。
然后我们放出求解器。它拿起产物 A，并试图用产物 B 去攻破它。首先是一次空泛性检查——确保这些断言不是平凡为真的（一种触发条件永不触发的“偷懒”式生成）。接着是有界模型检查，探索深层状态空间——深达 50、100 个周期——搜寻死锁、竞态条件和协议违规。
如果求解器找到一个 bug，它不只是标记出来。它会生成一段反例轨迹——一份精确的波形，展示这个 bug 究竟是如何显现的。而循环正是在这里闭合：我们把那段轨迹作为提示词回喂给 LLM。“你的设计失败了。这是轨迹：周期 1，Reset 撤销断言。周期 2，Request 拉高。周期 10，Grant 仍为低。grant 从未到来。修复这个状态机。”
LLM 分析这段轨迹，找出缺失的状态转换，重写代码。求解器再次检查。这个循环会自动重复，直到设计被证明为正确。
我在我们研究的交互式版本中对这一架构做了远为深入的阐述，但其核心洞见很简单：我们用 AI 来写证明，用数学来检查 AI。二者互不信任。彼此都让对方变得更好。
那些让我成为信徒的 bug
让我真正成为这套方法的信徒的，不是理论，而是我们捕获到的、其他任何手段都不可能发现的具体 bug。
开源 RISC-V 社区已经产出了一些确实卓越的处理器核心——Ibex（用于谷歌的 OpenTitan 安全芯片）、来自苏黎世联邦理工学院的 PULP 平台。这些都是背后有着真正工程实力、经过反复严格审视的设计。而它们依然含有只有形式化验证才能发现的 bug。
形式化验证咨询公司 Axiomise 在 Ibex 核心中发现了一个 bug：一个调试请求在分支指令期间的某个特定周期到达时，可能导致核心死锁或执行错误的指令。想想这意味着什么——一个安全关键的核心，经过数十名工程师审查，而一款形式化工具发现了仿真完全错过的一个 bug。
在 PULP 平台中，人们发现了一个 bug：在AWVALID与AWREADY交互的某种特定“繁忙”模式下，AXI 互连可能无限期地饿死某个总线主设备。这是一个经典的活性失效——系统不会崩溃，它只是停止取得任何进展。你绝不会针对那种特定的交互模式去写一个定向测试。可能的模式实在太多，根本无法一一列举。
当我们把 Veriprajna 对准一个 RISC-V 加载存储单元时，它会自动为接口合规性（“若 valid 被断言，它必须保持为高，直到 ready”）、数据完整性（“从地址 X 读出的数据与对地址 X 的最后一次写入一致”）以及前向进展（“该单元最终必须返回一个响应”）生成断言。这些并不是事后拴到代码上的东西。它们是与代码一同、从同一份规格说明生成的，并在任何一行 RTL 离开我们的系统之前就被强制执行。
关于我们方法论及形式化验证引擎的完整技术拆解，参见我们详细的研究论文。
“但形式化验证无法扩展”
人们总是在这一点上提出反驳，我也理解为什么。形式化验证素有计算量爆炸的名声——一颗现代 SoC 的状态空间大到天文数字，而朴素的形式化方法在任何比玩具级设计更大的东西上都会卡死。
我们在这方面投入了大量精力。我们的系统使用自动化抽象技术，让形式化验证在规模上变得可行。黑盒化让我们能够验证胶合逻辑，同时把 RAM 或复杂 ALU 这样的大型子模块当作具有已定义接口的抽象实体来处理。切割点打断 valid/ready 握手路径，使我们能够独立于数据处理来验证流控。对称性约简让我们能为多端口路由器的一个通道证明某个属性，再从数学上归纳出它对全部 N 个通道都成立。
它被彻底解决了吗？没有。模拟物理始终会带来形式化方法无法触及的挑战。但那些逻辑 bug——竞态条件、死锁、协议违规——在生成的代码中变得在数学上不可能存在。而这些正是导致重新流片的 bug。
我听到的另一个反对意见是关于速度。“运行一个形式化求解器难道不会拖慢设计流程吗？”是的，它会增加计算成本。但我愿意天天都用计算时间来换取进度上的确定性。一个多跑一个小时的形式化求解器，比一次六个月的重新流片要便宜无穷多。
关于“AI 设计的芯片”的那个令人不安的真相
行业里有一种正在获得越来越多认同的叙事——AI 很快就将端到端地设计芯片，我们正从计算机辅助设计走向计算机自动化设计。我认为这种叙事在方向上是对的，但危险地不完整。
我们正在朝着智能体化工作流构建，让自主 AI 智能体彼此协作——一个负责高层划分的架构师智能体、一个负责实现的 RTL 编码员、一个负责编写测试平台和断言的验证工程师、一个负责在功耗、性能和面积约束下统筹整个流程的管理者。我们使用检索增强生成（RAG）不仅是为了代码，也是为了知识——拉取特定的协议规则、工艺设计套件约束以及内部编码规范，好让 LLM 在不产生幻觉的前提下生成合规的代码。
但这一切都无法运作——没有一样能运作——如果缺了一根形式化验证的主心骨的话。AI 变得越自主，每一份输出在流向下游之前都经过数学验证这件事就越是至关重要。一个生成代码更快的 AI 智能体，只有在那些代码正确时才有价值。一个既生成代码更快、又证明其正确的 AI 智能体？那才是未来。
半导体行业的问题不在于 AI 写硬件代码太慢。而在于 AI 太快地写出了那些隐蔽地错误的硬件代码。
我们不是副驾。我们不是聊天机器人。我们是一家恰好把生成式 AI 用作前端的形式化验证晶圆厂。这个区别很重要，因为它决定了你在为什么而优化。副驾为速度而优化。我们为正确性而优化。在一个单个逃逸的 bug 就会造成 1000 万美元光罩损失和 5000 万美元营收损失的世界里，我很清楚我会选择哪一种优化。
抉择早已作出
半导体行业再也承受不起“生成后祈祷”的做法了。“十倍法则”不是一条建议——它是物理与经济学合谋惩罚任何流片未经验证的硅片的人。在 5nm 及以下、光罩组价格逼近 2000 万美元的当下，容错的余地已经坍缩为零。
每一周，我都会与那些设计团队交谈，他们既为 LLM 能给自己的生产力带来什么而兴奋，又为 LLM 可能给自己的流片进度带来什么而恐惧。他们同时怀有这两种感受是对的。这项技术确实是变革性的。但若没有安全网，它也确实是危险的。
Veriprajna 就是那张安全网。我们把 AI 的速度与数学的确定性一并交给你。不是“大概正确”。不是“通过了回归测试”。而是被证明为正确，跨越每一种可能的输入、每一种可能的状态、每一种仿真永远想不到去测试的边角情况。
如今摆在每一位芯片设计者面前的抉择，不是要不要用 AI。那艘船早已启航。抉择在于，是用一种能证明自己成果的 AI，还是用一种只会寄望于最好结果的 AI。
我很清楚我会拿 1000 万美元押注哪一种。
