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

TL;DR

Veri-Sure is a multi-agent framework that enhances RTL code correctness by combining contract-based intent alignment, localized repairs, and a hybrid verification pipeline, significantly improving verified code generation in EDA.

Contribution

It introduces Veri-Sure, a novel multi-agent system with contract enforcement, temporal tracing, and formal verification, advancing the reliability of LLM-assisted RTL design.

Findings

Achieves state-of-the-art verified RTL code generation performance.

Outperforms standalone LLMs and prior systems in correctness.

Extends benchmark with 53 industrial-grade tasks.

Abstract

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.