FormalRTL: Verified RTL Synthesis at Scale

FormalRTL is a novel end-to-end multi-agent framework that leverages software reference models as formal specifications to enable scalable, verified, and reliable register-transfer level (RTL) code generation for complex industrial hardware designs.

The Gist

Imagine you are trying to build a massive, incredibly complex skyscraper (a computer chip). In the past, you had to hire a team of architects and engineers to draw every single brick, beam, and wire by hand. It took years, cost a fortune, and if they made one tiny mistake in the blueprint, the whole building could collapse.

Recently, we discovered a magical new tool: an AI that can write blueprints just by listening to your description. But there's a catch. If you just tell the AI, "Build me a skyscraper with a glass roof," it might build a house, or a tower with a roof made of jelly. It's great at writing words, but it's terrible at understanding the strict laws of physics and engineering required to keep a building standing.

This is the problem the paper FormalRTL solves.

The Problem: The "Vague Instructions" Trap

Current AI tools try to turn human language directly into hardware code.

• The Issue: Human language is fuzzy. You might say "make it fast," but the AI doesn't know if that means "fast like a race car" or "fast like a cheetah."
• The Result: The AI generates code that looks okay but fails when tested. In the chip world, this is like building a bridge that looks beautiful but collapses when a truck drives over it.

The Solution: The "Golden Blueprint"

The authors of this paper realized that in the real world, engineers don't just guess. They have a "Golden Blueprint" (a software reference model written in C/C++). This is a perfect, mathematically proven simulation of how the chip should work before they ever build the real thing.

FormalRTL is a new system that acts like a super-smart construction foreman. Instead of letting the AI guess the blueprint, it forces the AI to follow the Golden Blueprint step-by-step.

How It Works: The Three-Worker Team

The system uses three specialized AI "agents" (workers) that talk to each other to build the chip:

1. The Planner (The Site Manager)

• What it does: Before building, the Planner looks at the Golden Blueprint (the C code) and breaks the giant skyscraper down into small, manageable rooms (sub-modules).
• The Analogy: Imagine you are baking a massive wedding cake. Instead of telling the baker, "Make the whole cake," the Planner says, "First, bake the bottom tier. Then, bake the middle tier. Finally, bake the top." It uses a map of the dependencies (what needs to be built before what) so the team never gets confused.

2. The Builder (The Mason)

• What it does: The Builder takes one small "room" (sub-module) and the Golden Blueprint for that specific room. It writes the actual hardware code (RTL) to build it.
• The Analogy: The Builder is a master mason. They look at the plan for the "kitchen" and lay the bricks. Crucially, they don't just guess; they build it so it matches the Golden Blueprint exactly.

3. The Inspector & Fixer (The Quality Control)

• What it does: This is the most important part. Once the Builder finishes a room, the Inspector immediately checks it against the Golden Blueprint.
  • If it matches: Great! Move to the next room.
  • If it fails: The Inspector doesn't just say "Wrong." It finds the exact brick that is out of place and tells the Builder, "You put a red brick where a blue one should be." The Builder then fixes it.
• The Analogy: Think of this like a spell-checker for math. If you write 2 + 2 = 5, a normal spell-checker might not catch it. But this Inspector is a math genius that instantly sees the error, points to the number 5, and says, "Change this to 4."

Why This is a Big Deal

• No More "Black Boxes": Old AI methods were like throwing darts in the dark. This method is like following a GPS.
• Scalability: They tested this on designs with over 1,000 lines of code (which is huge for AI). The system successfully built complex math chips (like those used in AI processors) that previous AI tools failed to create.
• Formal Proof: The system doesn't just "hope" the chip works; it mathematically proves the hardware matches the software blueprint. It's like having a guarantee from the universe that the bridge won't fall.

The Trade-off

The paper admits that the chips built by this AI aren't quite as perfectly optimized (smaller or faster) as chips built by a human genius engineer who has spent 20 years on the project.

• The Analogy: The AI-built chip is like a house built by a very fast, very accurate robot. It's 100% safe and functional, but a human architect might have squeezed in one extra closet or made the windows slightly larger.
• The Benefit: However, getting a working chip in days instead of years is a massive win. Engineers can then take this "good enough" base and tweak it to make it perfect.

Summary

FormalRTL is like giving an AI a strict, mathematically perfect recipe (the software model) and a team of specialized workers (planner, builder, inspector) to follow it. Instead of guessing how to build a computer chip, the AI is forced to prove, step-by-step, that its construction matches the recipe. This turns the chaotic process of "AI guessing" into a reliable, industrial-grade manufacturing line.

Technical Summary

Here is a detailed technical summary of the paper "FormalRTL: Verified RTL Synthesis at Scale".

1. Problem Statement

The design of complex, computation-intensive hardware (e.g., GPUs, NPUs) is becoming a bottleneck due to the pursuit of extreme Power, Performance, and Area (PPA) targets. While Large Language Models (LLMs) show promise in automating Register-Transfer Level (RTL) code generation, current research faces two critical barriers preventing industrial adoption:

• Large-Scale Design Complexity: Existing methods struggle with designs requiring thousands of lines of code. Purely natural language specifications are often ambiguous, leading to architectural errors when LLMs attempt to decompose complex tasks without a rigid structural guide.
• Lack of Formal Correctness Guarantees: Current approaches rely on simulation-based verification (testbenches), which often fails to cover corner cases, especially in datapath-heavy designs with intricate arithmetic logic. Unlike the industry standard, which uses software reference models (C/C++) for formal equivalence checking (EC), LLM-driven synthesis has largely ignored this resource.

2. Methodology: FormalRTL

The authors propose FormalRTL, a novel end-to-end multi-agent framework that integrates software reference models as formal, executable specifications to guide RTL synthesis. The system operates on a "bottom-up" verification philosophy, ensuring each submodule is formally equivalent to its C counterpart before integration.

The pipeline consists of four key components:

A. Planning Agent (Static Analysis-Driven)

Instead of relying solely on natural language, the Planning Agent performs static analysis on the C reference model using a compiler (Clang).

• It parses the Abstract Syntax Tree (AST) to identify function dependencies.
• It decomposes the complex design into modular subtasks based on the topological order of these dependencies.
• It refactors the high-level specification into targeted sub-specifications for each module, ensuring architectural decisions are grounded in the actual code structure.

B. Initializing Agent (Synthesis & Harness Generation)

For each submodule, this agent generates:

1. RTL Code: The Verilog implementation.
2. Verification Harness: A formal verification environment that assumes identical inputs for both the C model and the RTL, asserting output equivalence.

• Timeframe Determination: The agent analyzes the C model to determine the exact number of clock cycles required for results, enabling transactional equivalence checking for sequential logic.

C. Debugging Agent (Counterexample-Guided)

This agent closes the loop when the Equivalence Checking (EC) tool (hw-cbmc) detects a mismatch. It utilizes two specialized tools to assist the LLM:

• Bug Locator: Extracts specific code lines surrounding syntax errors to reduce the LLM's search burden.
• Counterexample (CE) Simplifier: Filters the EC report to show only the mismatching signals and relevant function states, helping the LLM pinpoint logic errors quickly.
• The LLM then generates a patch, which is applied and re-verified.

D. Formal Verification

The system uses hw-cbmc to perform rigorous equivalence checking between the software (C) and hardware (RTL) models. This provides a mathematical proof of functional correctness, replacing the probabilistic nature of simulation.

3. Key Contributions

1. Reference Model-Driven Methodology: The paper pioneers a workflow where software reference models (C/C++) act as the "golden specification" for LLM-based synthesis, bridging the gap between agile AI generation and rigorous industrial verification.
2. End-to-End Multi-Agent Engine: A unified framework that automates the entire lifecycle: static analysis planning, code generation, formal verification, and counterexample-guided debugging.
3. Industrial-Grade Benchmark Suite: The authors constructed and released a new benchmark suite containing complex datapath-intensive modules (e.g., FP16 operators, Hifloat8 arithmetic) derived from both academic sources (Berkeley Softfloat) and industrial scenarios (Ascend AI Chip). Each case includes a specification, a C reference model, and the target RTL.

4. Experimental Results

The framework was evaluated on a suite of benchmarks ranging from ~50 to over 1,000 lines of RTL code.

• Success Rates:
  • Initial Success Rate (ISR): While initial generation success varied (15%–90% depending on complexity), the system demonstrated high robustness.
  • Final Success Rate (FSR): The system achieved 95%–100% FSR for most modules within a 20-iteration limit, proving the effectiveness of the counterexample-guided debugging loop.
• Scalability & Planning:
  • Ablation Study: Compared against a baseline that treats the C model as unstructured text (specification-only), FormalRTL showed significantly higher stability. As design complexity increased (up to 1,130 lines), the baseline's success rate dropped to 0%, while FormalRTL maintained high success rates.
  • Bottom-Up Efficiency: The top-level modules often had higher initial success rates than leaf modules because their dependencies were already verified, reducing the implementation burden.
• Quality of Result (QoR):
  • LLM-generated RTL had slightly larger area and delay compared to manually optimized designs (e.g., ~36% larger area for hifloat8_mul).
  • However, the authors argue this is acceptable trade-off for obtaining a functionally correct, executable baseline, which accelerates the subsequent PPA optimization phase for human engineers.

5. Significance

FormalRTL represents a paradigm shift in automated hardware design by moving away from "simulation-based trial-and-error" toward "formal verification-driven synthesis."

• Bridging the Gap: It effectively narrows the gap between academic LLM prototypes and industrial-grade requirements by addressing the critical need for correctness guarantees.
• Scalability: The static analysis-based decomposition strategy allows LLMs to handle complex, multi-thousand-line designs that previously caused them to fail.
• Future Impact: By open-sourcing the framework and benchmarks, the authors provide a foundation for future research into specialized LLMs for debugging and the development of more robust open-source equivalence checking tools.

In conclusion, FormalRTL demonstrates that integrating formal methods (software reference models and EC) with multi-agent LLM workflows is a viable and necessary path toward scalable, automated hardware synthesis.