FormalRTL: Verified RTL Synthesis at Scale

TL;DR

FormalRTL introduces a multi-agent framework that leverages formal specifications and integrates planning, synthesis, and verification to enable scalable, reliable RTL code generation for complex industrial hardware designs.

Contribution

It presents a novel end-to-end framework combining formal specifications with hardware synthesis, addressing industrial-scale challenges in datapath-centric design.

Findings

Effective handling of complex industrial benchmarks

Scalable and reliable RTL code generation

Open-source framework and benchmark suite

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.