FormalRTL: Verified RTL Synthesis at Scale

Das Paper stellt FormalRTL vor, ein verifiziertes Multi-Agenten-Framework, das Software-Referenzmodelle als formale Spezifikationen nutzt, um die zuverlässige und skalierbare Generierung von industrietauglichem RTL-Code mittels großer Sprachmodelle zu ermöglichen.

Das Wesentliche

Stellen Sie sich vor, Sie wollen ein riesiges, hochkomplexes Schloss bauen – aber nicht aus Stein, sondern aus digitalen Schaltern und Leitungen. Das ist das, was Ingenieure tun, wenn sie Computerchips (wie die in Ihrem Handy oder einer KI) entwerfen. Die Sprache, in der diese Chips beschrieben werden, heißt RTL (Register-Transfer-Level). Sie ist extrem präzise, aber auch sehr schwer zu verstehen.

Bisher versuchten KI-Modelle (wie große Sprachmodelle), diese Chips einfach nur aus einer mündlichen Beschreibung zu bauen. Das war wie ein Architekt, der versucht, ein Wolkenkratzer-Grundriss zu zeichnen, indem er nur auf ein Foto schaut und sagt: „Mach mal was Großes." Das Ergebnis war oft chaotisch oder funktionierte gar nicht.

Hier kommt FormalRTL ins Spiel. Die Forscher von der Chinesischen Universität Hongkong und der Südost-Universität haben eine neue Methode entwickelt, die man sich wie einen perfekten Bauleiter mit einem magischen Prüfstein vorstellen kann.

Die drei Hauptakteure (Die Agenten)

Stellen Sie sich das Team von FormalRTL wie eine hochspezialisierte Baufirma vor:

1. Der Planer (Planning Agent): Der Architekt mit dem Bauplan

   • Das Problem: Wenn man einem KI-Modell sagt „Bau einen Prozessor", wird es verwirrt. Es weiß nicht, wo es anfangen soll.
   • Die Lösung: Der Planer schaut sich nicht nur die mündliche Beschreibung an, sondern nutzt einen Software-Referenzcode (geschrieben in C/C++). Das ist wie ein detaillierter, mathematisch korrekter Bauplan, der bereits in einer einfachen Sprache existiert.
   • Die Analogie: Statt das ganze Schloss auf einmal zu bauen, zerlegt der Planer den Bauplan in kleine, handhabbare Räume (Zellen, Treppen, Wände). Er sagt: „Zuerst bauen wir das Fundament, dann die erste Etage, dann das Dach." Er nutzt den Computer, um genau zu sehen, welche Teile voneinander abhängen, und erstellt eine perfekte Reihenfolge.

2. Der Ersteller (Initializing Agent): Der Maurer

   • Die Aufgabe: Dieser Agent baut nun jeden einzelnen Raum (Submodul) nach dem Bauplan.
   • Der Trick: Er baut nicht nur die Wände, sondern stellt sofort einen Testaufbau auf. Er vergleicht den neuen digitalen Raum sofort mit dem ursprünglichen Bauplan (dem C-Code).
   • Die Analogie: Es ist, als würde ein Maurer jeden Ziegelstein legen und sofort prüfen: „Passt dieser Stein genau in die Form, die der Bauplan vorschreibt?" Wenn ja, weiter. Wenn nein, sofort stoppen.

3. Der Fehlerfinder (Debugging Agent): Der Detektiv mit dem Röntgenblick

   • Das Problem: Manchmal passt etwas nicht. Bei normalen Tests sagt man nur: „Es funktioniert nicht." Aber warum?
   • Die Lösung: FormalRTL nutzt einen „formalen Prüfstein" (ein Werkzeug namens hw-cbmc). Wenn etwas falsch ist, liefert dieses Werkzeug nicht nur ein rotes Licht, sondern einen genauen Beweis (einen Gegenbeispiel).
   • Die Analogie: Stellen Sie sich vor, Ihr Auto springt nicht an. Ein normaler Mechaniker sagt: „Irgendetwas ist kaputt." Der Detektiv von FormalRTL sagt: „Der Zündschlüssel dreht sich, aber der Motor im Zylinder 3 hat den Druck verloren, weil ein Ventil klemmt."
   • Dieser Detektiv zeigt dem KI-Modell genau, wo der Fehler ist, und das Modell repariert es sofort. Dieser Kreislauf (Bauen -> Prüfen -> Reparieren) läuft so lange, bis alles perfekt ist.

Warum ist das so revolutionär?

Bisher waren KI-Entwürfe wie ein Wahrsager, der versucht, die Zukunft vorherzusagen. Er rät, und manchmal hat er Glück.
FormalRTL ist wie ein Ingenieur mit einem mathematischen Beweis.

• Kein Raten mehr: Da sie den C-Code als „Goldstandard" (eine unbestechliche Wahrheit) nutzen, muss die KI nicht raten, wie die Schaltung funktionieren soll. Sie muss nur den Code in eine andere Sprache übersetzen.
• Skalierbarkeit: Früher konnten KIs nur kleine Schaltungen (wie einen einfachen Rechner) bauen. Mit dieser Methode können sie jetzt riesige, industrielle Chips entwerfen, die Tausende von Zeilen Code haben, weil sie das Problem in kleine, lösbare Puzzleteile zerlegen.
• Sicherheit: Das Wichtigste: Am Ende haben sie einen formalen Beweis, dass der Chip genau das tut, was er soll. Es gibt keine „vielleicht"-Fehler mehr.

Das Fazit

Die Forscher haben also einen Weg gefunden, KI nicht nur als „Kreativschreiber" für Hardware zu nutzen, sondern als disziplinierten Übersetzer, der von einem perfekten mathematischen Modell geleitet wird.

Stellen Sie sich vor, Sie geben einer KI einen Kochrezept-Text (die Spezifikation) und eine perfekt gekochte Probe (den C-Code). Die KI muss nun das Rezept in eine Anleitung für einen Roboter-Koch (den Chip) übersetzen. Die KI schaut ständig auf die Probe, prüft jeden Schritt und korrigiert sich selbst, bis der Roboter-Koch das exakt gleiche Gericht serviert.

Das Ergebnis: Schnellere Entwicklung von Chips, weniger teure Fehler und eine neue Ära, in der KI uns hilft, die Hardware der Zukunft zu bauen – sicher, zuverlässig und bewiesen korrekt. Die Forscher werden ihre Werkzeuge und Testfälle bald für alle verfügbar machen, damit die ganze Welt davon profitieren kann.

Technische Zusammenfassung

Hier ist eine detaillierte technische Zusammenfassung des Papers „FormalRTL: Verified RTL Synthesis at Scale" auf Deutsch:

1. Problemstellung

Die Automatisierung der Hardware-Synthese mittels Large Language Models (LLMs) stößt bei industriellen, datenpfad-zentrierten Designs (z. B. für GPUs, NPUs, TPUs) an ihre Grenzen. Die bestehenden Forschungsansätze leiden unter zwei fundamentalen Herausforderungen:

• Komplexität großer Designs: Industrielle IP-Kerne erfordern oft Tausende Zeilen RTL-Code. Herkömmliche Planungsansätze scheitern an unklaren oder mehrdeutigen natürlichen Sprachspezifikationen und der Schwierigkeit von LLMs, fundierte architektonische Entscheidungen für komplexe Designs zu treffen.
• Fehlende formale Korrektheitsgarantien: Simulationen decken oft keine Randfälle (Corner Cases) ab, insbesondere bei tief verschachtelten Datapaths und benutzerdefinierten Datentypen (z. B. bfloat16, hifloat8). Direkte Synthese aus natürlicher Sprache kann die komplexen strukturellen, zeitlichen und arithmetischen Anforderungen nicht zuverlässig erfassen.

In der industriellen Praxis verlassen sich Ingenieure traditionell auf Software-Referenzmodelle (meist in C/C++), die als „Gold-Standard" für die formale Äquivalenzprüfung (Equivalence Checking, EC) dienen. Bisherige LLM-basierte Ansätze haben diese wertvolle Ressource weitgehend ignoriert.

2. Methodik: FormalRTL

Das Paper stellt FormalRTL vor, ein neuartiges End-to-End Multi-Agenten-Framework, das Software-Referenzmodelle als ausführbare formale Spezifikationen nutzt, um die RTL-Code-Generierung und -Verifikation zu steuern. Der Workflow besteht aus drei Hauptagenten:

• Planungs-Agent (Planning Agent):

  • Führt eine statische Analyse des C-Referenzmodells durch (unter Verwendung eines C-Compilers und des Abstract Syntax Tree, AST).
  • Zerlegt das komplexe Design in modulare Teilaufgaben basierend auf den funktionalen Abhängigkeiten.
  • Refaktoriert die Spezifikation für jedes Submodul, um architektonische Mehrdeutigkeiten zu minimieren.
  • Die Generierung erfolgt strikt in der topologischen Reihenfolge der Abhängigkeiten (Bottom-up-Ansatz).

• Initialisierungs-Agent (Initializing Agent):

  • Generiert für jedes Submodul den initialen RTL-Code und ein entsprechendes Verifikations-„Harness".
  • Das Harness stellt sicher, dass C- und RTL-Code identische Eingaben erhalten und die Ausgabeäquivalenz behauptet wird.
  • Bestimmt den erforderlichen Zeitrahmen (Clock Cycles) für sequentielle Logik, um die Tiefe der Pipelines zu steuern und transaktionale Äquivalenzprüfungen zu ermöglichen.

• Debugging-Agent (Debugging Agent):

  • Nutzt ein formales Äquivalenz-Checking-Tool (hw-cbmc), um Fehler zu identifizieren.
  • Erhält zwei Arten von Feedback: Syntaxfehler und Gegenbeispiele (Counterexamples) bei logischen Inkonsistenzen.
  • Verwendet einen Bug-Locator, um Syntaxfehler im Kontext zu zeigen, und einen CE-Simplifier, um Gegenbeispiele auf die relevanten Signale und Funktionen zu reduzieren.
  • Das LLM generiert basierend auf diesem Feedback Patches, die automatisch angewendet werden, bis die Äquivalenz erreicht ist.

3. Schlüsselbeiträge

• Neue Methodik: Pionierarbeit bei der Nutzung von Software-Referenzmodellen als treibende Kraft für agile Hardware-Entwicklung, die Skalierbarkeit und formale Korrektheit durch statische Analyse und Äquivalenzprüfung sicherstellt.
• Multi-Agenten-Engine: Entwicklung eines vollständig automatisierten Workflows, der Planung, Synthese, Debugging und formale Verifikation integriert.
• Benchmark-Suite: Erstellung und Veröffentlichung einer neuen Suite von industriellen Benchmarks (basierend auf akademischen Softfloat-Modulen und industriellen Hifloat8-Modellen), die sowohl Spezifikationen als auch C-Referenzmodelle enthalten.

4. Ergebnisse

Die Evaluation wurde auf einer Suite komplexer Module (bis zu über 1000 Zeilen RTL) durchgeführt:

• Effektivität des Debuggings: Der Debugging-Agent ist hochwirksam. Während die Initial Success Rate (ISR) bei komplexen Modulen oft niedrig ist (LLMs scheitern oft beim ersten Versuch), erreichen fast alle Module eine hohe Final Success Rate (FSR) innerhalb des Iterationslimits (z. B. 95–100% bei den meisten Modulen).
• Skalierbarkeit: Im Vergleich zu einem Baseline-Ansatz (nur Spezifikation, keine C-Analyse) zeigt FormalRTL eine überlegene Stabilität. Bei steigender Komplexität (bis Design 4 mit 1130 Zeilen) fiel die Erfolgsrate des Baseline-Ansatzes auf 0%, während FormalRTL auch bei großen Designs hohe Erfolgsraten beibehielt.
• Qualität (QoR): Die von LLMs generierten Designs weisen zwar in Bezug auf Fläche und Verzögerung (PPA) noch Lücken zu manuell optimierten Designs auf, bieten aber eine korrekte, ausführbare Basis. Dies ermöglicht Ingenieuren eine systematische Optimierung auf einer verifizierten „Goldenen Referenz".
• Ablationsstudien: Die Entfernung von Komponenten wie dem Counterexample-Simplifier oder der Gegenbeispiel-gesteuerten Debugging-Logik führte zu einer signifikanten Verschlechterung der Leistung (höhere Iterationszahlen, niedrigere Erfolgsraten).

5. Bedeutung und Ausblick

FormalRTL schließt die Lücke zwischen akademischen Prototypen und industriellen Anforderungen, indem es die Zuverlässigkeit formaler Verifikation mit der Flexibilität von LLMs verbindet.

• Industrielle Relevanz: Der Ansatz adressiert das kritische Problem der Korrektheit bei komplexen Datapaths, das bisherige LLM-Ansätze ignorierten.
• Zukunftsausblick: Die Autoren sehen Potenzial in der Entwicklung spezialisierter, kleinerer LLMs für das Debugging von Gegenbeispielen und in der Schaffung besserer Open-Source-Tools für die C-RTL-Äquivalenzprüfung.

Zusammenfassend demonstriert FormalRTL, dass die Integration von Software-Referenzmodellen in einen Multi-Agenten-Workflow eine skalierbare und verlässliche Methode für die automatische Synthese von industrietauglichem Hardware-Code darstellt.