Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair

Stellen Sie sich vor, Sie bauen eine riesige, komplizierte Burg aus digitalen Lego-Steinen. Das ist es, was Ingenieure tun, wenn sie Computerchips entwerfen: Sie schreiben Code namens RTL (Register Transfer Level), der den winzigen Transistoren sagt, wie sie sich verhalten sollen. Aber hier ist der Haken: Wenn auch nur ein einziger Stein an der falschen Stelle platziert wird, kann das ganze Schloss zusammenbrechen, sobald der Strom eingeschaltet wird. Das Aufspüren solcher Fehler ist der schwierigste Teil des Jobs und nimmt oft mehr als die Hälfte der Zeit in Anspruch. Traditionell nutzen Ingenieure zwei Hauptwege, um ihre Arbeit zu überprüfen. Der erste ist wie eine „Probefahrt“, bei der sie den Chip durch einige spezifische Szenarien laufen lassen, um zu sehen, ob er kaputtgeht. Der zweite ist die „formale Verifikation“, die einem super-mathematischen Beweis gleicht, der garantiert, dass die Burg unter jeder möglichen Bedingung stehen bleibt, nicht nur unter den, die sie getestet haben. Diese Super-Beweismethode erfordert jedoch meist teure, geschlossene Software, die sich nur große Unternehmen leisten können.

Hier kommt der neue Akteur auf den Plan: Large Language Models (LLMs). Sie kennen sie vielleicht als KI-Chatbots, die Geschichten oder Code schreiben können. Kürzlich begannen Menschen zu fragen: „Kann eine KI der Architekt sein, der unsere kaputten digitalen Burgen repariert?“ Die große Frage ist, ob eine KI nicht nur einen Fehler entdecken, sondern ihn auch so reparieren kann, dass er mathematisch perfekt bewiesen ist, ohne dass man eine Million-Dollar-Softwarelizenz kaufen muss. Dieses Paper taucht genau in diese Frage ein und versucht, eine Brücke zwischen der Kreativität der KI und der strengen, unnachgiebigen Logik der formalen Mathematik zu schlagen – und das ausschließlich mit kostenlosen Open-Source-Werkzeugen.

Der KI-Detektiv und das Open-Source-Werkzeugkasten

In dieser Studie hat ein Forscher namens Ha Trung Tran ein kluges Team von KI-Agenten aufgebaut, das als Reparaturtrupp für defekte Chip-Designs fungiert. Stellen Sie es sich wie ein hochtechnologisches Detektiv-Team vor, das in einer Schleife arbeitet. Anstatt dass eine einzige KI alles auf einmal versucht, ist das Team aufgeteilt: Ein Agent liest die Baupläne, ein anderer schreibt die Regeln dafür, was der Chip tun sollte, ein dritter überprüft die Arbeit und ein vierter repariert tatsächlich den Code.

Das Geheimrezept hier ist die Art und Weise, wie sie nach Fehlern suchen. Die meisten KI-Reparaturwerkzeuge führen lediglich ein paar Probefahrten (Simulationen) durch, um zu sehen, ob der Chip funktioniert. Aber dieses Team nutzt ein „formales Backend“ – eine kostenlose Open-Source-Mathematik-Engine, die aus Werkzeugen namens Yosys, SymbiYosys und Z3 besteht. Diese Engine rät nicht einfach; sie versucht mathematisch zu beweisen, dass der Chip korrekt ist. Wenn der Chip fehlschlägt, sagt die Engine nicht nur „er ist kaputt“. Sie übergibt der KI ein spezifisches „Gegenbeispiel“, das wie eine Video-Wiedergabe ist, die exakt zeigt, wie die Burg zusammengebrochen ist. Die KI schaut sich dann dieses Video an, findet heraus, was schiefgelaufen ist, und versucht, es zu reparieren. Sie wiederholen dies – prüfen, den Absturz finden, reparieren, erneut prüfen – bis die Mathematik beweist, dass der Chip perfekt ist oder ihnen die Versuche ausgehen.

Die guten Nachrichten: Es funktioniert (manchmal)

Die Forscher testeten dieses System an sechs verschiedenen Arten von digitalen Designs, die von einem einfachen Rechenteil (einer ALU) bis hin zu komplexeren Verkehrssteuerungen und Speichereinheiten reichten. Die Ergebnisse waren eine Mischung aus Triumph und deutlichen Einschränkungen.

Der Star der Show war die ALU (Arithmetic Logic Unit), die wie das Rechengehirn eines Chips funktioniert. Die Forscher haben sie absichtlich manipuliert, indem sie eine „UND“-Operation durch eine „ODER“-Operation ersetzten. Das KI-Team entdeckte den Fehler sofort. In nur zwei Runden aus Überprüfung und Reparatur reparierte es den Code.ت Viel wichtiger war, dass die Open-Source-Mathematik-Engine mit 100-prozentiger Sicherheit bewies, dass die Korrektur für jede mögliche Zahl, die der Chip jemals verarbeiten könnte, korrekt war. Dies geschah in allen fünf Testläufen und dauerte im Durchschnitt nur 16,5 Sekunden. Es bewies, dass die Idee funktioniert: Eine KI, geleitet von Open-Source-Mathematik-Tools, kann einen echten Bug finden und mit einem mathematischen Garantien reparieren.

Die schlechten Nachrichten: Wo die KI stecken blieb

Die Geschichte ist jedoch kein totaler Sieg. Als die Forscher denselben Prozess bei den anderen fünf Designs versuchten, stieß das KI-Team gegen eine Wand. Sie konnten keine davon zuverlässig reparieren. Das Paper analysiert sorgfältig, warum sie scheiterten, und identifiziert vier verschiedene „Fehlermodi“, die wie Fallen für die KI wirken:

1. Die „Zu tief“-Falle (Bounded-Cover Vacuity): In einem Fall (ein Counter) sagte die Mathematik-Engine „FAIL“, obwohl die Korrektur eigentlich korrekt war. Warum? Weil das Design 256 Zyklen laufen musste, um einen bestimmten Zustand zu erreichen, aber das Tool nur 256 Zyklen tief blickte. Es war, als würde man versuchen zu beweisen, dass ein Auto ein Land durchqueren kann, indem man nur eine Meile weit fährt; das Tool konnte das Ziel nicht sehen, also gab es auf. Das Paper merkt an, dass dies ein Limit des Tools ist, nicht der KI.
2. Die „Verwirrende Anweisungen“-Falle (Specification Ambiguity): Bei einem anderen Design (einem Arbiter) versuchte die KI, den geschriebenen Regeln zu folgen, aber die Regeln verlangten etwas Unmögliches (wie eine Ampel, die sich ohne Uhrzeit ändert). Die KI folgte pflichtbewusst den unmöglichen Anweisungen, was in einer Sackgasse endete.
3. Die „Zeitreise“-Falle (Temporal Logic Bugs): In zwei Fällen (einem UART-Transmitter und einem FIFO-Speicher) betrafen die Bugs Ereignisse, die über mehrere Zeitschritte hinweg stattfanden. Die KI war gut darin, Logik-Schritte einzelner Momente zu reparieren (wie beim Taschenrechner), aber sie hatte Schwierigkeiten, über Sequenzen von Ereignissen zu argumentieren, die über die Zeit ablaufen.
4. Die „Zu viele Regeln“-Falle (Multi-Property Pressure): Im letzten Fall (einem AXI Lite Slave) gab es so viele Regeln, denen der Chip gleichzeitig entsprechen musste, dass das Reparieren einer Regel eine andere brach. Die KI geriet in eine Schleife, da sie nicht in der Lage war, eine Lösung zu finden, die alle zufriedenstellte.

Ein versteckter Fehler im Werkzeugkasten

Es gab auch eine überraschende Entdeckung über die Open-Source-Tools selbst. Die Forscher fanden heraus, dass das Yosys-Tool, das bei der Verarbeitung des Codes hilft, eine versteckte Eigenart besitzt. Wenn man versucht, die Sicherheitsprüfungen (Assertions) mit einer speziellen Methode namens „bind“ an das Design anzuhängen, ignoriert das Tool diese stillschweigend. Es ist, als würde man eine Sicherheitskamera in einen Raum stellen, aber die Kamera ist ausgesteckt; das System denkt, alles sei in Ordnung, weil es die Kamera nie sieht. Die Forscher mussten ihre Methode ändern und die Prüfungen direkt in den Code „injizieren“, um sicherzustellen, dass die Mathematik-Engine sie tatsächlich sieht. Dies ist ein hilfreicher Tipp für jeden, der diese kostenlosen Tools verwendet.

Das Fazit

Dieses Paper ist eine „Machbarkeitsstudie“, was eine schicke Art zu sagen ist: „Wir haben es versucht, und hier ist genau, wo es funktioniert und wo es scheitert.“ Die wichtigste Erkenntnis ist, dass es möglich ist, eine KI zur Reparatur von Chip-Designs mit einem mathematischen Korrektheitsbeweis einzusetzen, aber nur, wenn man Open-Source-Werkzeuge verwendet und wenn das Problem nicht zu komplex ist.

Der Autor ist ehrlich über die Grenzen: Das System ist großartig darin, einfache, unmittelbare Logikfehler zu beheben (wie den Taschenrechner), aber es hat derzeit Schwierigkeiten mit komplexen Timing-Problemen, tiefen Speicherzuständen oder Designs mit widersprüchlichen Regeln. Er behauptet nicht, das Problem der Chip-Reparatur gelöst zu haben; stattdessen hat er eine klare Karte gezeichnet, die die „Sicherheitszone“, in der die KI arbeitet, und die „Gefahrenzone“, in der sie sich verliert, aufzeigt. Durch die Verwendung ausschließlich kostenloser Tools hoffen sie, die Eintrittshürden für diese Art von Forschung zu senken und zu beweisen, dass man kein Millionen-Dollar-Budget benötigt, um die Zukunft des zuverlässigen Hardware-Designs zu gestalten.