🤖 AI

Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation

Veri-Sure 是一个具备契约感知能力的多智能体框架，它通过设计契约对齐智能体意图、通过静态依赖切片执行精确的局部修复，并利用基于追踪的时序分析与形式化验证的混合流水线来验证输出，从而确保硅级 RTL 的正确性，且该框架是在新引入的工业级 VerilogEval-v2-EXT 基准测试上进行评估的。

原作者： Jiale Liu, Taiyu Zhou, Tianqi Jiang

发布于 2026-01-28

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Jiale Liu, Taiyu Zhou, Tianqi Jiang

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正试图根据一套用纯英文编写的指令，制造一台复杂、高速的机器（比如一个未来的机器人）。你要求一个超级聪明的 AI 将这些指令转化为机器真正的蓝图（代码）。

问题在于，这个 AI 虽然擅长写句子，但它经常在蓝图中留下微小且隐形的错误，这些错误只有在机器全速运转时才会显现。在真实的芯片设计领域，这些错误代价极其高昂——一旦芯片制造完成，修复它们的成本可能高达数百万美元。

这篇论文介绍了一个名为 VERI-SURE 的全新“AI 专家团队”，旨在这些错误在芯片制造之前就将其修复。以下是它的工作原理，我们使用简单的类比来解释：

1. 问题所在：“传声筒游戏”与“盲点”

当你要求单个 AI 编写代码时，会出现两个问题：

传声筒游戏（Telephone Game）： 如果你要求 AI 修复一个漏洞（bug），它可能会误解你的原始目标。它为了修复一件事而修改了代码，却不小心破坏了最初的意图。
盲点（Blind Spot）： AI 通常通过运行模拟（试驾）来检查自己的工作。但就像一次试驾可能会错过在特定颠簸路面上才会发生的罕见引擎故障一样，模拟往往会错过那些只在现实世界中才会发生的棘手时序错误。

2. 解决方案：专业的施工团队

VERI-SURE 并没有让一个 AI 承担所有工作，而是建立了一个每个成员都有特定职责的施工队。他们首先会对一份**“设计合同”**达成一致。

建筑师（合同制定者）： 在任何人开始编写任何一行代码之前，这个智能体负责将你杂乱的英文指令转化为一份严格的数学“合同”。它定义了机器应该如何表现、按钮的功能以及运行速度。这确保了团队中的每个人都在阅读同一张地图。
程序员（建造者）： 这个智能体根据合同编写实际的蓝图（代码）。
校验员（安全检查员）： 这个智能体负责进行试驾（模拟）。如果机器失败了，它不会只说“它坏了”，它还会分析崩溃数据。

3. 妙招：“外科手术式修复” vs. “拆除重建”

当试驾失败时，旧的 AI 系统通常会陷入恐慌，尝试拆除整座建筑并从头开始。这样做风险很大，因为它们可能会忘记如何正确建造墙壁。

VERI-SURE 使用的是外科手术式修复：

侦探（追踪分析）： 它观察“黑匣子”数据（波形），找到机器失效的具体时刻。
外科医生（依赖切片）： 它不是靠猜测，而是通过回溯线路来找到导致问题的确切那一小块代码。它隔离出那个微小的部分。
补丁： AI 只重写那块微小的、损坏的代码。机器的其他部分保持原封不动。这防止了“传声筒游戏”中那种“修好一个东西却弄坏另一个”的情况。

4. 超级检查：“数学证明” vs. “试驾”

有时，仅仅靠试驾不足以证明一台机器是安全的。

断言器（规则执行者）： 这个智能体检查机器是否遵循时间规则（例如：“灯是否在按下按钮时准时亮起？”）。
布尔证明器（数学巫师）： 对于逻辑部分，这个智能体不只是运行测试；它使用数学证明来保证代码在任何输入下都绝不可能出错。这就像是用物理方程证明一座桥永远不会坍塌，而不是仅仅开车在上面开过一次。

5. 新的测试赛道：“更难的障碍赛”

为了证明他们的团队是最优秀的，作者构建了一个更难的障碍赛道，名为 VERILOGE EVAL-V2-EXT。

旧的测试就像是在停车场里驾驶（任务简单、短暂）。
新的测试包括在暴风雨中驾驶、在迷宫中导航以及搬运重型货物（工业级的任务，如复杂的通信协议和内存控制）。

结果

当他们把他们的团队（VERI-SURE）放在这个新的、困难的障碍赛道上时：

独立 AI（孤独的天才）大约完成了 76% 的任务。
旧的 AI 团队（没有外科手术式修复或数学证明的团队）在处理最难的任务时表现挣扎。
VERI-SURE 实现了 93% 的成功率，即使是在最困难、最复杂的任务上也是如此。

简而言之： VERI-SURE 不仅仅是要求 AI “编写代码”。它创建了一个纪律严明的团队，他们达成计划共识，通过外科手术式修复仅针对损坏的部分进行修复，并利用数学来证明修复是完美的，从而确保最终的芯片完全按照预期工作。

技术摘要：VERI-SURE

1. 问题陈述

将大语言模型（LLM）部署于电子设计自动化（EDA）中的寄存器传输级（RTL）设计，在实现硅级正确性方面面临显著障碍。尽管 LLM 在软件代码生成领域已取得长足进步，但 RTL 生成由于硬件的并发特性、严格的周期级时序以及协议语义，呈现出独特的挑战。本文识别了当前基于 LLM 的 RTL 流水线中的三个主要瓶 much 瓶颈：

评估可靠性有限： 以仿真为中心的评估往往存在测试覆盖率不足的问题，无法捕捉细微的时序边界情况（corner cases）。
调试效率低下： 迭代调试经常导致由“回归与修复幻觉”引起的失效，这是由于全文件重构会导致无关逻辑发生不稳定变化。
语义漂移： 随着自然语言意图在多次智能体（agent）交接或迭代中被重新解读，原始的设计意图可能会发生退化，导致实现不一致。

现有的基准测试（如 VerilogEval-v2）被批评为过度由短小的、教学性质的模块所主导，未能代表工业级需求，如高级算术单元、通信协议和时钟域交叉（CDC）模式。

2. 方法论：VERI-SURE 框架

VERI-SURE 是一个契约感知（contract-aware）的多智能体框架，旨在闭合从代码合成、验证到局部修复的环路。它超越了一次性翻译，转向自动化的“生成-验证-调试”循环。

核心组件

设计契约（架构智能体/Architect Agent）： 框架首先将自然语言规范提炼为结构化的 JSON 格式设计契约。该契约明确定义了接口语义、时钟/复位约定、周期精确行为及边界情况。它作为所有后续智能体的共享“事实来源”，以防止语义漂移。
多智能体工作流：
- 编码智能体（Coder Agent）： 根据契约生成可综合的 RTL 代码。
- 验证智能体（Verifier Agent）： 生成与契约对齐的自检测试平台（testbenches）。
- 调试智能体（Debugger Agent）： 当仿真失败时，引导自主调试循环。
- 断言智能体（Asserter Agent）： 生成针对性的 SystemVerilog 断言，以检测时序或协议违规（例如：错误的边沿采样、复位不匹配）。
- 布尔证明智能体（Boolean Proofer Agent）： 对组合逻辑进行形式验证，以验证候选修复方案并防止回归。

关键机制

追踪驱动的时序分析与静态切片： 当仿真失败时，系统不仅依赖文本日志。它通过分析波形变化转储（VCD）来识别最早的偏差时间（ $t_f$ ）。随后，它采用静态依赖切片来计算影响失效信号的“逻辑锥”（cone of logic）。这能将失效隔离到最小的怀疑代码块（行范围）中，而非整个文件。
局部补丁（Localized Patching）： 在切片分析的指导下，调试智能体仅对怀疑的代码块应用精确的、块级的编辑（读取/替换）。这避免了全文件重写带来的不稳定性。回滚规则确保只有当补丁能够改善失效特征（例如：更晚的首个失败时间或更少的失配）时，才会被保留。
多分支验证： 框架集成了两个验证分支：
1. 追踪驱动的时序分析： 用于处理时序和顺序问题。
2. 形式验证： 结合基于断言的检查（通过 Asserter）和布尔等价证明（通过使用 SymbiYosus 的 Boolean Proofer），以验证组合逻辑约束并证明超越有限仿真的正确性。

3. 基准测试：VERILOGEVAL-V2-EXT

为了更好地评估工业级 RTL 生成，作者引入了 VERILOGEVAL-V2-EXT。该基准测试扩展了原始的 VerilogEval-v2，增加了 53 个新的工业级设计任务，使总数达到 209 个问题。

内容： 新任务涵盖了复杂的领域，如通信协议（UART、FIFO）、高级算术、DSP 内核以及多周期数据通路。
分层： 问题根据结构化信号（代码行数、assign/always 块数量、数据通路宽度）和人工评审被划分为简单、中等和困难三个难度等级。这允许进行更细粒度的失效模式分析。

4. 实验结果

作者将 VERI-SURE 与 15 个独立的 LLM（包括商业闭源模型和开源权重模型）、单智能体反馈循环以及先前的多智能体系统（MAGE, VerilogCoder）进行了对比评估。

性能： VERI-SURE 在 VERILOGEVAL-V2-EXT 基准测试上实现了 93.30% 的功能性 Pass@1，且语法成功率为 100%。
困难任务： 该框架在“困难”任务上表现出最大的优势，实现了 85.07% 的功能通过率，显著优于表现最好的独立模型（Gemini-3-Pro，为 62.69%）和其他智能体基准。
骨干模型无关性： 虽然 VERI-SURE 在使用 GPT-5.2 时表现最佳，但它也显著提升了开源权重模型 DeepSeek-3.2 的性能，将其功能通过率从 61.24%（独立运行时）提升至 71.29%。
消融实验：
- 移除追踪、切片与补丁机制导致了最大的性能下降（整体下降 11.0%，困难任务下降 16.4%），证实了精确定位的重要性。
- 移除形式验证使困难任务的通过率降低了 11.9 个百分点，证明了其在调试仿真无法发现的深层逻辑错误方面的必要性。
- 移除契约机制导致整体性能下降 2.9%，凸显了其在维持意图一致性方面的作用。

5. 重要性与主张

论文声称，VERI-SURE 通过从以仿真为中心的评估转向结合追踪驱动分析与形式验证的混合方法，证明了自动化 RTL 设计可以更接近“硅级正确性”。

主要主张包括：

缓解语义漂移： 通过强制执行结构化设计契约，框架统一了智能体的意图，防止了需求的逐渐重新解读。
修复的稳定性： 由依赖切片引导的补丁机制有效地降低了与全文件重构相关的回归风险和修复幻觉。
超越仿真： 形式证明的集成使得系统能够以纯仿真无法实现的方式验证功能正确性，特别是对于组合等价性和复杂的时序约束。
工业相关性： 引入 VERILOGEVAL-V2-EXT 为评估端到端 RTL 生成能力提供了一个更真实且具辨别力的测试平台，填补了学术基准与工业 IP 模块需求之间的空白。

作者总结道，虽然大规模预训练提供了强大的基础，但结合形式验证的结构化智能体工作流对于实现复杂、多周期硬件设计的高可靠性至关重要。