Btor2MLIR: A Format and Toolchain for Hardware Verification

Stellen Sie sich vor, Sie sind ein Detektiv, der versucht, ein Rätsel zu lösen, aber die Hinweise sind in einem Geheimcode geschrieben, den nur wenige Spezialisten lesen können. In der Welt der Informatik ist dieser „Geheimcode“ die Sprache, die beschreibt, wie Computerchips (Hardware) sich verhalten sollen. Ingenieure bauen diese Chips, um alles von Ihrem Telefon bis hin zu Satelliten im Weltraum anzutreiben, aber wenn es auch nur einen winzigen Fehler im Design gibt, kann das gesamte System abstürzen oder seltsam reagieren. Um dies zu verhindern, nutzen Forscher „formale Methoden“ – mathematische Werkzeuge, die wie supergeladene Rechtschreibprüfungen fungieren, um zu beweisen, dass ein Design perfekt ist, bevor es jemals gebaut wird.

Lange Zeit sprachen diese Rechtschreibprüfer unterschiedliche Sprachen. Einige sprachen „BTOR2“, ein Format, das in Hardware-Wettbewerben beliebt ist, während andere eine Sprache namens „LLVM-IR“ sprachen, die von Software-Compilern verwendet wird, um Code zu prüfen. Es war, als hätte man einen Übersetzer, der nur Deutsch nach Englisch übersetzen kann, und einen anderen, der Spanisch nach Englisch übersetzt. Wenn man einen französischen Übersetzer nutzen wollte, um ein spanisches Buch zu prüfen, wäre man aufgeschmissen gewesen. Man musste jedes Mal einen völlig neuen Übersetcher von Grund auf neu bauen. Dieses Paper stellt einen neuen, magischen Übersetzer namens BTOR2MLIR vor. Er sitzt in der Mitte und fungt als universelle Brücke, die es Hardware-Designs ermöglicht, mit Software-Tools zu kommunizieren, ohne dass man jedes Mal das Rad neu erfinden muss.

Das Problem: Zu viele Dialekte, nicht genug Brücken

In der Welt der Hardware-Verifizierung ist das BTOR2-Format zum Standard geworden, um Schaltkreise für Wettbewerbe wie den Hardware Model Checking Competition (HWMCC) zu beschreiben. Betrachten Sie BTOR2 als einen sehr spezifischen, effizienten Dialekt, um zu beschreiben, wie ein digitaler Schaltkreis zählt, Zahlen addiert oder Fehler prüft. Tools wie BTORMC wurden speziell entwickelt, um diesen Dialekt zu lesen und zu prüfen, ob der Schaltkreis sicher ist.

Die Welt der Software-Verifizierung ist jedoch riesig und leistungsstark. Tools wie SEAHORN sind Experten darin, Software-Code zu prüfen, der in der Sprache LLVM-IR geschrieben ist. Diese Tools sind unglaublich ausgereift und wurden über Jahrzehnte durch massive Projekte wie die LLVM-Compiler-Infrastruktur verfeinert. Sie verfügen über eingebaute Funktionen zur Optimierung von Code, zum Finden von Bugs und zum Ausführen von Simulationen.

Das Problem ist, dass diese beiden Welten selten miteinander sprechen. Um ein leistungsstarkes Software-Tool zu verwenden, um ein Hardware-Design zu prüfen, mussten Forscher kundenspezifische, einmalige Übersetzer schreiben. Es war, als versuche man, einen quadratischen Steckzapfen in ein rundes Loch zu passen. Diese Übersetzer mussten oft Basisfunktionen (wie den Umgang mit Zahlen oder Schleifen) neu implementieren, die bereits in den Software-Tools existierten, was zu verschwendeter Arbeit und potenziellen Fehlern führte.

Die Lösung: Der universelle Adapter (BTOR2MLIR)

Die Autoren dieses Papers, Joseph Tafese, Isabel Garcia-Contreras und Arie Gurfinkel von der University of Waterloo, beschlossen, eine bessere Brücke zu bauen. Sie entwickelten BTOR2MLIR, ein neues Format und eine Toolchain basierend auf MLIR (Multi-Level Intermediate Representation).

Um MLIR zu verstehen, stellen Sie sich ein riesiges, modulares Lego-Set vor. Anstatt jedes Mal ein ganzes neues Schloss von Grund auf neu zu bauen, wenn Sie ein anderes Haus bauen wollen, gibt Ihnen MLIR eine Basis aus Bausteinen (Dialekten), die Sie zusammenstecken können. Sie können einen neuen „Hardware“-Baustein definieren, der exakt wie BTOR2 aussieht und sich so verhält, aber direkt in die bestehende „Software“-Lego-Struktur passt.

So funktioniert ihr neues Tool:

1. Der Übersetzer: Sie haben einen „BTOR-Dialekt“ innerhalb von MLIR gebaut. Dies ist eine direkte, verlustfreie Übersetzung des BTOR2-Formats. Wenn Sie eine BTOR2-Datei haben, kann BTOR2MLIR diese sofort in diesen MLIR-Dialekt umwandeln.
2. Die Brücke: Da MLIR darauf ausgelegt ist, erweiterbar zu sein, haben sie einen „Conversion Pass“ erstellt, der ihren BTOR-Dialekt in den Standard-LLVM-Dialekt umwandelt. Dies ist der magische Schritt. Er nimmt die Hardware-Beschreibung und verwandelt sie in ein Format, das Software-Tools wie SEAHORN nativ verstehen können.
3. Das Ergebnis: Das Ergebnis ist LLVM-IR, eine Sprache, die Software-Verifizierungs-Engines „verzehren“ und analysieren können.

Das Experiment: Funktioniert es tatsächlich?

Das Team hat nicht nur die Brücke gebaut; sie sind mit einem Lkw darüber gefahren, um zu sehen, ob sie hält. Sie nahmen eine Sammlung von realen Hardware-Benchmarks aus dem HWMCC-Wettbewerb (speziell die Sets von 2019 und 2020) und leiteten sie durch ihre neue Toolchain.

Zuerst prüften sie die Korrektheit. Sie nahmen eine BTOR2-Datei, konvertierten sie in ihr MLIR-Format und konvertierten sie dann zurück zu BTOR2. Sie verglichen die ursprüngliche und die „Round-tripped“ Datei. Das Ergebnis? Sie waren identisch. Die Sicherheits-Eigenschaften (die Regeln, denen der Schaltkreis folgen muss) wurden perfekt bewahrt. Selbst in kniffligen Fällen, in denen die ursprünglichen Tools ein Timeout verursachten oder den Speicher überforderten, lösten ihre Round-tripped-Versionen das Problem manchmal sogar, was darauf hindeutet, dass die Übersetzung keine Fehler eingeführt hat.

Als Nächstes testeten sie die Leistung. Sie verbanden ihr Tool mit SEAHORN, einem berühmten Software-Model-Checker, und BOOLECTOR, einem schnellen Solver. Sie verglichen diese neue „hybride“ Pipeline mit BTORMC, dem Goldstandard-Tool, das speziell für BTOR2 gebaut wurde.

Die Ergebnisse waren überraschend und ermutigend:

• Geschwindigkeit: In vielen Fällen war die hybride Pipeline (BTOR2MLIR + SEAHORN + BOOLECTOR) konkurrenzfähig mit und manchmal sogar schneller als das dedizierte BTORMC-Tool. Beispielsweise löste der hybride Ansatz in der Kategorie „19/mann“ der Benchmarks 44 Instanzen in etwa 3.190 Sekunden, während BTORMC bei mehr Instanzen länger brauchte oder ein Timeout verursachte.
• Flexibilität: Das Tool bewältigte erfolgreich komplexe Operationen wie Division und Bitvektoren, was bewies, dass die „Lego-Steine“ von MLIR die schwere Arbeit der Hardware-Logik leisten können.
• Einschränkungen: Die Autoren waren ehrlich darüber, was ihr Tool noch nicht kann. Es unterstützt derzeit Bitvektoren und Arrays, behandelt aber noch nicht „Fairness“- und „Justice“-Constraints (Regeln darüber, wie sich ein System über unendliche Zeit verhält). Außerdem, obwohl es gut funktioniert, hat es die spezialisierten Hardware-Tools in keiner Kategorie komplett „zerlegt“; es war ein starker Konkender, kein totaler Ersatz.

Warum das wichtig ist

Das Paper behauptet nicht, die gesamte Hardware-Verifizierung gelöst zu haben. Stattdessen schlägt es eine neue Denkweise vor. Durch die Nutzung der ausgereiften, robusten Infrastruktur des LLVM-Compilers (der die Tools für alles von Videospielen bis hin zu Webbrowsern antreibt), können Hardware-Forscher aufhören, das Rad neu zu erfinden.

Die Autoren zeigen, dass man ein Hardware-Design nehmen, es in eine universelle Sprache übersetzen und dann leistungsstarke, existierende Software-Tools verwenden kann, um es zu prüfen. Dies öffnet die Tür für schnelles Prototyping. Wenn ein Forscher eine neue Verifizierungstechnik ausprobieren möchte, muss er keinen völlig neuen Motor bauen; er muss lediglich seine Idee in das MLIR-Framework einbinden.

In Zukunft plant das Team, diese Brücke mit noch mehr Tools zu verbinden, wie etwa KLEE (eine Symbolic-Execution-Engine) und LIBFUZZER (ein Fuzzing-Tool), die derzeit für Software verwendet werden, aber die Art und Weise, wie wir Bugs in Hardware finden, revolutionieren könnten. Sie planen auch, andere Formate wie AIGER und SMT-LIB zu generieren.

Letztendlich ist BTOR2MLIR ein Beweis dafür, dass die Mauern zwischen Hardware- und Software-Verifizierung fallen. Es deutet darauf an, dass wir durch das Sprechen einer gemeinsamen Sprache unsere digitale Welt sicherer, schneller und einfacher gestaltbar machen können.