Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

FormalRTL: Verified RTL Synthesis at Scale

Kezhi Li, Min Li, Xiangyu Wen, Shibo Zhao, Jieying Wu, Junhua Huang, Qiang Xu

TL;DR

This work presents FormalRTL, a novel end-to-end multi-agent framework that systematically integrates software reference models as formal, executable specifications to guide register-transfer level (RTL) code generation and verification.

Abstract

Large language models (LLMs) have demonstrated significant potential in automating hardware synthesis, yet substantial barriers remain for industrial-scale, datapath-centric designs due to ambiguous specifications and a lack of formal correctness guarantees. In this work, we present FormalRTL, a novel end-to-end multi-agent framework that systematically integrates software reference models as formal, executable specifications to guide register-transfer level (RTL) code generation and verification. By tightly coupling planning, synthesis, and formal equivalence checking, FormalRTL achieves scalable and reliable hardware code generation that addresses the critical challenges faced in industrial contexts. The comprehensive evaluation of a new suite of complex industrial-grade benchmarks demonstrates the effectiveness and robustness of our approach. We will open-source the FormalRTL framework and the benchmark suite to facilitate future research in this area.

FormalRTL: Verified RTL Synthesis at Scale

TL;DR

This work presents FormalRTL, a novel end-to-end multi-agent framework that systematically integrates software reference models as formal, executable specifications to guide register-transfer level (RTL) code generation and verification.

Abstract

Large language models (LLMs) have demonstrated significant potential in automating hardware synthesis, yet substantial barriers remain for industrial-scale, datapath-centric designs due to ambiguous specifications and a lack of formal correctness guarantees. In this work, we present FormalRTL, a novel end-to-end multi-agent framework that systematically integrates software reference models as formal, executable specifications to guide register-transfer level (RTL) code generation and verification. By tightly coupling planning, synthesis, and formal equivalence checking, FormalRTL achieves scalable and reliable hardware code generation that addresses the critical challenges faced in industrial contexts. The comprehensive evaluation of a new suite of complex industrial-grade benchmarks demonstrates the effectiveness and robustness of our approach. We will open-source the FormalRTL framework and the benchmark suite to facilitate future research in this area.
Paper Structure (18 sections, 5 equations, 4 figures, 3 tables)

This paper contains 18 sections, 5 equations, 4 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. LLM for RTL Synthesis
  4. Multi-agent Approaches for RTL Synthesis
  5. Software in Hardware Development
  6. Proposed Methods
  7. Planning Agent
  8. Initializing Agent
  9. Debugging Agent
  10. Benchmark Curation
  11. Experiments
  12. Experimental Setup
  13. Metrics
  14. Performance on Module-level Cases
  15. Ablation Study of Planning Methods
  16. ...and 3 more sections

Figures (4)

  • Figure 1: The general workflow of FormalRTL. The central pipeline (middle) takes a C model and specification, then iteratively generates, verifies, and debugs RTL code on a per-submodule basis. The planning agent (right) uses C static analysis (AST) to intelligently partition the main task. The debugging agent (left) leverages feedback from equivalence checking, using counterexamples to automatically guide an LLM in generating code patches.
  • Figure 2: Submodule implementation flow guided by C function dependencies.
  • Figure 3: Qualitatively demonstrate bug localization and counterexample simplification.
  • Figure 4: Comparison of planning methods on fixing iterations and FSR.