Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Jiale Liu, Taiyu Zhou, Tianqi Jiang

TL;DR

The paper tackles silicon-grade RTL code generation by LLMs, identifying limitations in simulation-based evaluation, regressions, and semantic drift. It introduces Veri-Sure, a contract-aware multi-agent framework that couples synthesis with trace-driven temporal analysis and formal verification, including assertion-based timing checks and Boolean equivalence proofs, to enable precise, localized repairs via static dependency slicing. It also extends the VerilogEval-v2 benchmark with 53 industrial-grade tasks (VerilogEval-v2-EXT) and demonstrates state-of-the-art verified RTL generation performance, achieving 93.30% overall functional Pass@1 and strong gains on hard problems. The results show that localized patching guided by formal hints and a contract-driven workflow can substantially improve RTL correctness and reduce regression risk in industrial EDA workflows.

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.

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

TL;DR

The paper tackles silicon-grade RTL code generation by LLMs, identifying limitations in simulation-based evaluation, regressions, and semantic drift. It introduces Veri-Sure, a contract-aware multi-agent framework that couples synthesis with trace-driven temporal analysis and formal verification, including assertion-based timing checks and Boolean equivalence proofs, to enable precise, localized repairs via static dependency slicing. It also extends the VerilogEval-v2 benchmark with 53 industrial-grade tasks (VerilogEval-v2-EXT) and demonstrates state-of-the-art verified RTL generation performance, achieving 93.30% overall functional Pass@1 and strong gains on hard problems. The results show that localized patching guided by formal hints and a contract-driven workflow can substantially improve RTL correctness and reduce regression risk in industrial EDA workflows.

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.
Paper Structure (75 sections, 12 equations, 5 figures, 11 tables)

This paper contains 75 sections, 12 equations, 5 figures, 11 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Automatic RTL Code Generation
  4. Tool-Integrated LLM Systems for HDL
  5. The Veri-Sure Framework
  6. Overall Architecture
  7. Contract Design
  8. Tracing, Static Slicing & Patching
  9. Trace-driven Temporal Analysis
  10. Static Dependency Slicing
  11. Localized Patching
  12. Formal Verification
  13. Asserter for Timing Supervision
  14. Boolean Proofer for Combinational Equivalence
  15. The VerilogEval-v2-EXT Benchmark
  16. ...and 60 more sections

Figures (5)

  • Figure 1: An overview of our Veri-Sure framework.
  • Figure 2: The tracing, static slicing and patching mechanism.
  • Figure 3: VerilogEval-v2-EXT problem taxonomy.
  • Figure 4: Dataset complexity statistics comparing the original one and ours (full extended dataset). (a--e) show distributions over problems for different metrics and (f) reports the Verilog construct coverage.
  • Figure 5: Case study: formal-hint-guided debugging in Veri-Sure. Boolean Proofer and Asserter agents help generate correct RTL code.