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

📄 arXiv: 2601.19747v1 📥 PDF

作者: Jiale Liu, Taiyu Zhou, Tianqi Jiang

分类: cs.AR, cs.AI, cs.SE

发布日期: 2026-01-27

💡 一句话要点

提出Veri-Sure框架，通过形式化验证提升LLM在RTL代码生成中的正确性。

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: RTL代码生成 形式化验证 多Agent系统 静态依赖切片 电子设计自动化

📋 核心要点

  1. 现有RTL代码生成方法依赖仿真，测试覆盖率有限，难以保证芯片级正确性，且迭代调试易引入回归问题。
  2. Veri-Sure框架通过设计契约对齐多Agent意图，并利用静态依赖切片进行精确修复，减少语义漂移。
  3. Veri-Sure集成了基于跟踪的时间分析和形式化验证，在扩展的VerilogEval-v2-EXT基准上超越了现有方法。

📝 摘要（中文）

在快速发展的电子设计自动化(EDA)领域，使用大型语言模型(LLM)进行寄存器传输级(RTL)设计已成为一个有前景的方向。然而，芯片级的正确性仍然受到以下因素的限制：(i)以仿真为中心的评估的测试覆盖率和可靠性有限，(ii)迭代调试引入的回归和修复幻觉，以及(iii)在代理切换过程中意图被重新解释而产生的语义漂移。在这项工作中，我们提出了Veri-Sure，一个多代理框架，它建立了一个设计契约来对齐代理的意图，并使用静态依赖切片指导的修补机制来执行精确的局部修复。通过集成一个多分支验证管道，该管道结合了基于跟踪的时间分析与包含基于断言的检查和布尔等价证明的形式化验证，Veri-Sure实现了超越纯仿真的功能正确性。我们还引入了VerilogEval-v2-EXT，通过53个更多的工业级设计任务和分层难度级别扩展了原始基准，并表明Veri-Sure实现了最先进的验证正确的RTL代码生成性能，超过了独立的LLM和先前的代理系统。

🔬 方法详解

问题定义：论文旨在解决使用大型语言模型（LLM）生成寄存器传输级（RTL）代码时，难以保证代码功能正确性的问题。现有方法主要依赖于仿真进行验证，但仿真覆盖率有限，无法充分验证代码的正确性。此外，在多Agent协作的场景下，由于Agent之间意图理解的偏差和迭代调试引入的回归问题，导致代码质量难以保证。

核心思路：论文的核心思路是通过引入设计契约来对齐多Agent的意图，并结合静态依赖切片技术进行精确的代码修复，从而减少语义漂移和回归问题。同时，采用多分支验证管道，结合基于跟踪的时间分析和形式化验证，以更全面地验证RTL代码的功能正确性。

技术框架：Veri-Sure框架包含以下主要模块：1) 设计契约模块：用于明确定义设计目标和约束，确保多Agent对设计意图的理解一致。2) 多Agent协作模块：多个Agent根据设计契约协同完成RTL代码的生成和验证任务。3) 静态依赖切片模块：用于分析代码的依赖关系，指导代码修复过程，减少修复引入的副作用。4) 多分支验证管道：包含基于跟踪的时间分析和形式化验证（包括基于断言的检查和布尔等价证明），用于全面验证RTL代码的功能正确性。

关键创新：Veri-Sure的关键创新在于：1) 引入设计契约来对齐多Agent的意图，减少语义漂移。2) 利用静态依赖切片技术进行精确的代码修复，避免引入新的错误。3) 集成多分支验证管道，结合基于跟踪的时间分析和形式化验证，提高验证的覆盖率和可靠性。

关键设计：设计契约的具体形式未知，但推测包含对RTL模块的功能描述、时序约束、接口定义等信息。静态依赖切片算法的具体实现未知，但推测使用了数据流分析和控制流分析等技术。多分支验证管道中，基于断言的检查和布尔等价证明的具体方法未知，但推测使用了现有的形式化验证工具和技术。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

Veri-Sure在扩展的VerilogEval-v2-EXT基准测试中取得了最先进的验证正确的RTL代码生成性能，超越了独立的LLM和先前的Agent系统。具体性能数据未知，但论文强调了其在工业级设计任务上的优越性，表明该框架具有很强的实用价值。

🎯 应用场景

Veri-Sure框架可应用于各种数字电路和系统的RTL代码自动生成，例如处理器、存储器、通信接口等。该研究成果有助于提高RTL代码的质量和开发效率，降低芯片设计的成本和风险，加速电子产品的上市时间。未来，该框架可进一步扩展到更复杂的SoC设计和异构计算系统。

📄 摘要（原文）

In the rapidly evolving field of Electronic Design Automation (EDA), the deployment of Large Language Models (LLMs) for Register-Transfer Level (RTL) design has emerged as a promising direction. However, silicon-grade correctness remains bottlenecked by: (i) limited test coverage and reliability of simulation-centric evaluation, (ii) regressions and repair hallucinations introduced by iterative debugging, and (iii) semantic drift as intent is reinterpreted across agent handoffs. In this work, we propose Veri-Sure, a multi-agent framework that establishes a design contract to align agents' intent and uses a patching mechanism guided by static dependency slicing to perform precise, localized repairs. By integrating a multi-branch verification pipeline that combines trace-driven temporal analysis with formal verification consisting of assertion-based checking and boolean equivalence proofs, Veri-Sure enables functional correctness beyond pure simulations. We also introduce VerilogEval-v2-EXT, extending the original benchmark with 53 more industrial-grade design tasks and stratified difficulty levels, and show that Veri-Sure achieves state-of-the-art verified-correct RTL code generation performance, surpassing standalone LLMs and prior agentic systems.