Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair

想象一下，你正在用数字乐高积木搭建一座宏伟而复杂的城堡。这就是工程师设计计算机芯片时所做的工作：他们编写被称为 RTL（寄存器传输级）的代码，告诉微小的晶体管该如何运作。但问题在于，如果哪怕只有一个积木放错了位置，整个城堡在通电时都可能崩塌。检查这些错误是这项工作中最难的部分，往往占据了超过一半的时间。传统上，工程师使用两种主要方法来检查他们的工作。第一种就像是“试驾”，即通过运行几个特定的场景来观察芯片是否会损坏。第二种是“形式验证”，这是一种超级数学证明，保证你的城堡在所有可能的条件下都能屹立不倒，而不仅仅是测试过的那些情况。然而，这种超级证明方法通常需要昂贵且封闭的软件，只有大公司才负担得起。

于是，出现了这位领域里的新面孔：大语言模型（LLM）。你可能知道它们是能够写故事或代码的 AI 聊天机器人。最近，人们开始询问：“AI 能否成为修复我们破碎数字城堡的建筑师？”核心问题在于，AI 是否不仅能发现错误，还能以一种经过数学证明是完美的方式来修复它，而不需要购买价值百万美元的软件许可。这篇论文深入探讨了这个问题，试图在 AI 的创造力与形式数学那严谨、不容置疑的逻辑之间架起一座桥梁，并且仅使用免费的开源工具。

AI 侦探与开源工具箱

在这项研究中，研究员 Ha Trung Tran 构建了一个聪明的 AI 智能体团队，充当损坏芯片设计的维修队。把它想象成一个高科技侦探小队，在一个循环中工作。与其让一个 AI 同时尝试完成所有事情，不如将团队进行分工：一个智能体阅读蓝图，另一个编写芯片“应该”遵循的规则，第三个检查工作，第四个则负责实际修复代码。

这里的秘诀在于他们如何检查错误。大多数 AI 维修工具只是运行几次“试驾”（模拟）来看看芯片是否正常工作。但这个团队使用了一个“形式化后端”——这是一个由 Yosys、SymbiYosus 和 Z3 等工具组成的免费开源数学引擎。这个引擎不仅仅是在猜测，它试图从数学上证明芯片是正确的。如果芯片失败了，引擎不会只说“它坏了”，而是会向 AI 提供一个具体的“反例”（counterexample），这就像是一段视频回放，准确地展示了城堡是如何崩塌的。随后，AI 会观看这段视频，弄清楚哪里出了问题，然后尝试修复它。他们不断重复这个过程——检查、寻找崩溃点、修复、再次检查——直到数学证明芯片是完美的，或者他们用完了尝试次数。

好消息：它奏效了（有时）

研究人员在六种不同类型的数字设计上测试了这个系统，范围从简单的计算器部件（ALU）到更复杂的流量控制器和存储单元。结果既有成功的喜悦，也有明显的局限性。

全场的明星是 ALU（算术逻辑单元），它就像是芯片的计算大脑。研究人员故意破坏了它，将一个“与”（AND）操作替换成了“或”（OR）操作。AI 团队立即发现了这个错误。在仅仅两轮的检查与修复后，他们就修复了代码。更重要的是，开源数学引擎以 100% 的确定性证明了该修复对于芯片可能处理的每一个数字都是正确的。这种情况在所有五次测试运行中都发生了，平均耗时仅 16.5 秒。这证明了这一构想是可行的：一个由开源数学工具引导的 AI，确实可以找到并修复一个真实的漏洞，并提供数学上的保证。

坏消息：AI 在哪里碰壁了

然而，故事并非完全的胜利。当研究人员在其他五种设计上尝试同样的过程时，AI 团队撞到了墙。他们无法可靠地修复其中任何一个。论文仔细分析了他们失败的原因，识别出了四个充当 AI 陷阱的“失效模式”：

1. “过深”陷阱（有界覆盖空虚性/Bounded-Cover Vacuity）： 在一个案例（计数器）中，尽管修复方案实际上是正确的，但数学引擎却显示“失败”。为什么？因为该设计需要运行 256 个周期才能达到特定状态，但工具只查看了 256 个周期之深。这就像试图通过只开一英里车程来证明一辆车可以横跨整个国家；工具看不见目的地，所以放弃了。论文指出，这是工具本身的限制，而非 AI 的问题。
2. “指令混乱”陷阱（规范歧义性/Specification Ambiguity）： 对于另一个设计（仲裁器），AI 试图遵循书面规则，但规则要求的却是一件不可能完成的事（比如一个没有时钟驱动的交通灯）。AI 忠实地遵循了这些不可能的指令，从而陷入了死胡同。
3. “时空穿越”陷阱（时序逻辑错误/Temporal Logic Bugs）： 在两个案例（UART 发送器和 FIFO 存储器）中，错误涉及跨越多个时间步的事件。AI 非常擅长修复单步逻辑（如计算器），但在推理随时间变化的事件序列方面却显得力不从心。
4. “规则过多”陷阱（多属性压力/Multi-Property Pressure）： 在最后一个案例（AXI Lite 从机）中，芯片必须同时遵守如此多的规则，以至于修复一个规则就会破坏另一个规则。AI 陷入了循环，无法找到一个能让所有人满意的解决方案。

工具箱中的隐藏缺陷

关于开源工具本身，还有一个意外的发现。研究人员发现，用于处理代码的 Yosys 工具有一个隐藏的怪癖。如果你尝试使用一种称为“绑定”（bind）的特定方法将安全检查（断言）附加到设计中，该工具会默默地忽略它们。这就像是在房间里安装了一个监控摄像头，但摄像头没插电一样；系统认为一切正常，因为它根本看不到摄像头。研究人员不得不改变方法，直接将检查“注入”到代码中，以确保数学引擎确实看到了它们。对于任何使用这些免费工具的人来说，这都是一个非常有用的提示。

总结

这篇论文是一项“可行性研究”，这是一种专业的说法，意为：“我们尝试了，并且这里是具体哪里有效，哪里会失效。” 主要结论是：使用 AI 来修复芯片设计并提供正确性的数学证明是可能的，但前提是你必须使用开源工具，且问题不能过于复杂。

作者诚实地说明了局限性：该系统非常擅长修复简单的、即时的逻辑错误（如计算器），但目前在处理复杂的时序问题、深层内存状态或具有冲突规则的设计时仍显吃力。他们并没有声称已经解决了芯片修复的难题；相反，他们绘制了一张清晰的地图，标出了 AI 工作的“安全区”和迷失方向的“危险区”。通过仅使用免费工具，他们希望降低此类研究的门槛，证明你不需要百万美元的预算也能开始构建可靠硬件设计的未来。