用合约约束多智能体，实现可验证的高可靠RTL代码生成
Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation
- 通过设计合约与依赖切片，精准定位并修复错误
- 结合时序追踪与形式化验证，正确率超越纯仿真方法
- 适合芯片设计自动化、LLM辅助硬件开发人群
在电子设计自动化领域，大语言模型用于寄存器传输级（RTL）设计展现出巨大潜力，但硅级正确性仍受三大瓶颈制约：(i) 以仿真为中心的评估测试覆盖不足且不可靠；(ii) 迭代调试引入回归与修复幻觉；(iii) 智能体间交接导致语义漂移。本文提出Veri-Sure，一个基于合约的多智能体框架，通过静态依赖切片引导修补机制实现精准局部修复。融合多分支验证流程，结合追踪驱动的时序分析与形式化验证（包含断言检查和布尔等价性证明），实现超越纯仿真的功能正确性保障。我们还构建了VerilogEval-v2-EXT基准，扩展53个工业级设计任务并分层难度，实验表明Veri-Sure在已验证正确代码生成方面优于独立大模型及现有智能体系统。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。