💬 NLP

CktFormalizer: Autoformalization of Natural Language into Circuit Representations

CktFormalizer ist ein Framework, das Lean 4s abhängigkeitstypisierte HDL nutzt, um LLMs bei der Generierung von Hardwarebeschreibungen zu leiten, die garantiert syntaktisch korrekt sind, frei von Synthese störenden Defekten sind und durch maschinengeprüfte Beweise funktional verifiziert werden, wodurch eine nahezu perfekte Backend-Realisierbarkeit erreicht und eine sichere, automatisierte PPA-Optimierung ermöglicht wird.

Ursprüngliche Autoren: Jing Xiong, Qi Han, Chenchen Ding, He Xiao, Zunhai Su, Chaofan Tao, Ngai Wong

Veröffentlicht 2026-05-11

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Jing Xiong, Qi Han, Chenchen Ding, He Xiao, Zunhai Su, Chaofan Tao, Ngai Wong

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie bitten einen sehr talentierten, aber etwas nachlässigen Architekten, einen Bauplan für ein Haus auf Basis einer mündlichen Beschreibung zu zeichnen.

In der traditionellen Welt des Chip-Designs würden Sie den Architekten bitten, die Anweisungen in Verilog zu verfassen (eine Sprache zur Beschreibung von Computerchips). Der Architekt mag eine wunderschöne Beschreibung verfassen, doch da Verilog eher wie ein loser Satz von Regeln ist, könnte der Architekt versehentlich sagen: „Verbinden Sie ein 4-Zoll-Rohr mit einem 8-Zoll-Rohr" oder „Erstellen Sie einen Flur, der in sich selbst zurückführt."

Der Computer prüft die Grammatik und sagt: „Sieht gut aus!" Doch wenn das Haus tatsächlich gebaut wird (der Chip hergestellt wird), führen diese Fehler dazu, dass die Rohre platzen oder der Flur Menschen gefangen hält. Dies sind teure, stille Ausfälle, die sich erst Wochen später zeigen.

CKTFORMALIZER ist ein neues Framework, das das Spiel verändert. Anstatt dem Architekten zu erlauben, direkt in der losen Sprache Verilog zu schreiben, zwingt es ihn, in einer strengen, mathematischen Sprache namens Lean zu schreiben.

So funktioniert es, anhand einer einfachen Analogie:

1. Der strenge Editor (der Compiler)

Stellen Sie sich Lean als einen super-strengen Editor vor, der genau weiß, wie ein Haus muss gebaut werden.

Der alte Weg: Der Architekt schreibt „Verbinden Sie Rohr A mit Rohr B." Der Editor prüft die Größen nicht. Später stellt das Bauteam fest, dass Rohr A zu klein ist.
Der CKTFORMALIZER-Weg: Der Architekt versucht zu schreiben „Verbinden Sie Rohr A (Größe 4) mit Rohr B (Größe 8)." Der Editor knallt sofort die Tür zu und sagt: „Fehler! Sie können diese nicht verbinden. Korrigieren Sie es jetzt."
Das Ergebnis: Der Architekt (eine KI) erhält sofortiges Feedback. Er kann nicht weitermachen, bis die Größen perfekt übereinstimmen. Dies fängt „Breiten-Mismatches" und „Schleifen" ein, bevor auch nur ein einziger Ziegelstein verlegt wird.

2. Das Sicherheitsnetz (Typsicherheit)

Im alten System könnten Sie versehentlich eine Tür in einem Raum offen lassen, und das Haus wird mit einem zugigen, defekten Raum gebaut. Im Lean-System sind die Regeln so streng, dass es physikalisch unmöglich ist, einen Bauplan mit einem defekten Raum zu verfassen.

Wenn der Architekt vergisst zu beschreiben, was passiert, wenn ein Schalter umgelegt wird, sagt der Editor: „Sie haben einen Fall übersehen! Sie müssen jede Möglichkeit beschreiben."
Dies stellt sicher, dass das Design „korrekt durch Konstruktion" ist. Wenn es kompiliert (die Prüfung des Editors besteht), ist es garantiert strukturell solide.

3. Der Beweis der Wahrheit (Formale Verifikation)

Normalerweise prüfen Sie, ob ein Hausdesign funktioniert, indem Sie ein kleines Modell bauen und testen. Manchmal funktioniert das Modell, aber das echte Haus nicht.
CKTFORMALIZER verwendet mathematische Beweise. Die KI rät nicht einfach; sie schreibt einen mathematischen Beweis, der besagt: „Dieses neue, billigere Design tut exakt das Gleiche wie das ursprüngliche perfekte Design."

Es ist, als hätte man einen Mathematiker, der beweist, dass Ihr neues, billigeres Bauplan zu 100 % funktional identisch mit dem Original ist, bis auf das letzte Atom, für jedes mögliche Szenario, nicht nur für die, die Sie getestet haben.

4. Der Optimierungszyklus (der intelligente Renovator)

Sobald die KI ein Design hat, das funktioniert, hört das System nicht auf. Es agiert wie ein intelligenter Renovator, der den Bauplan betrachtet und sagt: „Wir können dieses Haus um 35 % verkleinern und 30 % weniger Energie verbrauchen."

Die KI versucht, die Räume (die Schaltunglogik) neu anzuordnen.
Sie baut eine neue Version.
Sie führt sofort wieder den „Strengen Editor" aus, um sicherzustellen, dass die neue Version immer noch perfekt funktioniert.
Anschließend führt sie eine physikalische Simulation durch, um zu sehen, wie viel Platz und Leistung sie spart.
Wenn die neue Version besser ist und mathematisch bewiesen korrekt bleibt, behält sie sie. Wenn nicht, wird sie zurückgesetzt.

Die Ergebnisse

Die Studie testete dies an hunderten von Designproblemen (wie dem Bau von Zählern, Speichereinheiten und Ampelsteuerungen).

Die Basislinie (alter Weg): Als sie versuchten, die Chips zu bauen, scheiterten etwa 20 % der Designs, die auf dem Papier korrekt aussahen, tatsächlich beim Versuch der Herstellung.
CKTFORMALIZER (neuer Weg): 100 % der Designs, die den strengen Editor bestanden, schafften es durch den gesamten Herstellungsprozess (Synthese, Platzierung und Routing), ohne zu versagen.
Effizienz: Das System gelang es zudem, die Designs erheblich zu verkleinern und Energie zu sparen (bis zu 35 % weniger Fläche), während es bewies, dass sie weiterhin perfekt waren.

Zusammenfassung

CKTFORMALIZER ist, als würde man einer KI-Architektin ein magisches Regelbuch geben, das sie daran hindert, Fehler zu machen, bevor sie überhaupt mit dem Zeichnen beginnt. Anstatt ein Haus zu bauen und zu hoffen, dass es nicht einstürzt, zwingt es den Architekten, zu beweisen, dass das Haus solide ist, bevor der erste Ziegelstein bestellt wird. Dies verwandelt das Chip-Design von einem Spiel des „Ratens und Prüfens" in einen Prozess des „Beweisens und Baus", was zu Chips führt, die kleiner, effizienter und garantiert funktionsfähig sind.

Technische Zusammenfassung: CktFormalizer

Problemstellung

Hardware-Design bleibt eine fehleranfällige Disziplin, bei der subtile Defekte wie Bit-Breiten-Mismatches, kombinatorische Schleifen oder unvollständige Falllogik in endlichen Automaten (FSMs) Syntaxprüfungen bestehen können, aber während der Synthese stillschweigend versagen oder später als kostspielige Silizium-Bugs auftreten. Während Large Language Models (LLMs) die Fähigkeit demonstriert haben, Verilog aus natürlichen Sprachspezifikationen zu generieren, erbt der resultierende Code oft die inhärenten Fallstricke von Verilog und VHDL: das Fehlen statischer Garantien wie abhängiger Typen, exhaustiver Musterabgleich und maschinengeprüfter Beweise. Folglich erfordert LLM-generierte Hardware häufig umfangreiches manuelles Debugging und scheitert oft daran, eine physische Implementierung (Place-and-Route, DRC, LVS) zu erreichen, selbst wenn sie in der Simulation funktional korrekt ist.

Methodik

Die Arbeit stellt CktFormalizer vor, ein Framework, das LLM-gesteuerte Codegenerierung mit formaler Verifikation vereint, indem es eine in Lean 4 eingebettete, abhängig getypte Hardware-Beschreibungssprache (HDL) zum Ziel hat. Anstatt direkt Verilog zu generieren, leitet das System den LLM-Agenten um, Lean-Code zu erzeugen, der als primäres Kompilierungsziel dient.

Kernarchitektur

Das Framework arbeitet durch eine geschlossene Schleifen-Pipeline, die drei distincte Rollen für Lean umfasst:

Typprüfer (Laufzeit-Verifizierer): Das abhängige Typsystem von Lean kodiert Bit-Breiten-Beschränkungen, Fallabdeckung und Azyklizität. Hardware-Defekte (z. B. Breiten-Mismatches oder kombinatorische Schleifen) werden als Kompilierungszeit-Typfehler erkannt, anstatt als stille Backend-Fehler. Dies bietet dem LLM-Agenten unmittelbares, handlungsorientiertes Feedback, um das Design iterativ zu reparieren.
Korrektheits-Firewall: Designs, die erfolgreich in Lean kompilieren, sind strukturell garantiert frei von bestimmten Defektklassen (Breiten-Mismatches, kombinatorische Schleifen, unbeabsichtigte Latches). Dies stellt sicher, dass kompilierte Designs den Backend-Synthese- und Place-and-Route (P&R)-Flow ohne die bei der Baseline-Verilog-Generierung beobachtete Verlustquote von 20 % überstehen.
Beweisassistent: Der Agent konstruiert automatisierte Theorembeweise, um die funktionale Äquivalenz zwischen der natürlichen Sprachspezifikation und der generierten (oder optimierten) Implementierung zu verifizieren. Diese Beweise decken beliebige Eingabesequenzen und parametrisierte Breiten ab und gehen über die Grenzen von SMT-basierten, beschränkten Prüfungen hinaus.

Arbeitsablauf

Generierung & Iteration: Ein LLM-Agent (instantiiert mit Claude) generiert Lean-HDL-Code basierend auf einer natürlichen Sprachspezifikation. Er betritt eine iterative „Generieren-Kompilieren-Reparieren"-Schleife, in der Lean-Kompilatorfehler den Agenten anleiten, semantische Bugs zu beheben, bevor sie sich fortpflanzen.
Extraktion: Nach erfolgreicher Kompilierung extrahiert ein Metaprogramm (#synthesizeVerilog) synthetisierbaren SystemVerilog aus dem Lean-Signal-Kombinator-Graphen.
Physische Implementierung: Der extrahierte SystemVerilog wird simuliert, synthetisiert (unter Verwendung von Yosys) und physisch implementiert (unter Verwendung von OpenROAD mit dem SkyWater 130nm PDK), um GDSII-Layouts und Power-Performance-Area (PPA)-Metriken zu generieren.
PPA-Optimierungsschleife: Eine geschlossene Optimierungsschleife speist PPA-Metriken zurück zum Agenten. Der Agent schlägt Architekturvarianten vor (z. B. parallele vs. serielle Datenpfade) und muss maschinengeprüfte Äquivalenzbeweise vorlegen, um sicherzustellen, dass die optimierte Variante funktional äquivalent zur ursprünglichen Spezifikation bleibt.

Hauptbeiträge

Erstes End-to-End-Framework: CktFormalizer ist das erste Framework, das LLM-gesteuerte Hardware-Generierung mit einer in Lean eingebetteten HDL kombiniert und eine Pipeline von natürlicher Sprache zu synthetisierbarem Silizium mit geschlossener PPA-Optimierungsschleife bietet.
Typgeleitete Generierung: Die Arbeit demonstriert, dass die Ausrichtung auf eine typsichere HDL die Erfolgsraten von LLMs im Vergleich zur direkten Verilog-Generierung erheblich verbessert. Kompilierungszeit-Typfehler liefern strukturiertes Feedback, das den Agenten zu korrekten Designs führt und auf branchenrelevante IP wie Multi-Channel-Handshake-Bus-Schnittstellen skaliert.
Integration formaler Verifikation: Das Framework schließt die Lücke zwischen LLM-generiertem Code und nachweisbar korrekter Hardware, indem es dem Agenten ermöglicht, maschinengeprüfte Äquivalenzbeweise zu erstellen. Dies stellt sicher, dass Architekturoptimierungen die funktionale Korrektheit nicht beeinträchtigen.

Experimentelle Ergebnisse

Das Framework wurde an drei Benchmarks evaluiert: VerilogEval (156 Probleme), RTLLM (50 Probleme) und ResBench (56 Probleme).

Backend-Realisierbarkeit: Ein entscheidendes Ergebnis ist, dass CktFormalizer die funktionale Korrektheit durch das Backend hinweg bewahrt. Während die Baseline (direkte Verilog-Generierung) etwa 20 % der funktional korrekten Designs während Synthese und Routing verliert, bewahrt CktFormalizer 100 % seiner kompilierten Designs durch den gesamten Synthese-, P&R-, DRC- und LVS-Flow.
Kompilierung und Simulation: Auf VerilogEval erreichte CktFormalizer eine Lean-Kompilierungsrate von 92,3 % und eine RTL-Simulationsbestehensrate von 72,4 %, was mit Baselines der direkten Verilog-Generierung konkurrenzfähig ist. Wenn Synthese-Feedback in die Agentenschleife einbezogen wird, steigt die Kompilierungsrate auf 99,4 %.
PPA-Optimierung: Die geschlossene Optimierungsschleife erzielte signifikante Verbesserungen. Durch validierte Architekturerkundung erreichte das Framework eine Flächenreduzierung von bis zu 35 % und eine Leistungsreduzierung von 30 %.
Timing-Closure: Alle funktional korrekten Designs, die Place-and-Route abschlossen, erreichten ohne manuelle Eingriffe Timing-Closure (WNS $\ge$ 0 ns).
Beweisgenerierung: In einer Pilotstudie verbesserte die schrittweise Beweisgenerierung (iterative Verfeinerung mit Beweisziel-Feedback) die Beweiserfolgsraten von 53 % auf 63 % und demonstrierte die Machbarkeit von Beweisassistenten für die Hardware-Verifikation.

Bedeutung und Behauptungen

Die Arbeit behauptet, dass abhängige Typen und LLM-Agenten komplementär sind. Durch die Verwendung einer formalen Sprache (Lean) sowohl als Generierungsziel als auch als Verifikationsuntergrund verwandelt das Framework die „Generieren-und-Testen"-Schleife des LLM von einer stochastischen Suche über syntaktisch gültige Programme in einen typgeleiteten Verfeinerungsprozess.

Die Autoren betonen, dass der Compiler als Verifizierer fungiert und die Fehlererkennung vom Ende des EDA-Pipelines (wo Korrekturen kostspielig sind) auf die Kompilierungszeit verlagert. Dieser Ansatz ermöglicht es dem System, Hardware zu produzieren, die nicht nur funktional korrekt, sondern auch strukturell robust gegenüber Backend-Transformationen ist und effektiv das Problem des „stillschweigenden Versagens" löst, das bei LLM-generierter Hardware üblich ist. Die Arbeit legt nahe, dass formale Sprachen als Grundlage für vertrauenswürdige, automatisierte Hardware-Designs dienen können, die es LLMs ermöglichen, die komplexen Zielkonflikte der Hardware-Optimierung zu navigieren, während strenge Korrektheitsgarantien gewahrt bleiben.