QiMeng-CodeV-SVA: Training Specialized LLMs for Hardware Assertion Generation via RTL-Grounded Bidirectional Data Synthesis

Die Arbeit stellt QiMeng-CodeV-SVA vor, ein Framework zur Synthese von Trainingsdaten durch RTL-gestützte bidirektionale Übersetzung, mit dem spezialisierte Modelle entwickelt wurden, die bei der Generierung von SystemVerilog-Assertions aus natürlicher Sprache (NL2SVA) fortschrittliche LLMs übertreffen.

Das Wesentliche

Stellen Sie sich vor, Sie bauen ein riesiges, hochkomplexes Schloss aus Legosteinen. Das ist ein Computerchip (Hardware). Bevor Sie das Schloss in die reale Welt schicken, müssen Sie sicherstellen, dass es nicht einstürzt, wenn jemand versehentlich an einem falschen Stein zieht.

In der Welt der Chip-Entwicklung nennt man diese Sicherheitsregeln Assertions (Sicherheitsprüfungen). Sie werden in einer sehr strengen, fast wie eine Fremdsprache wirkenden Sprache geschrieben, die SystemVerilog Assertions (SVA) heißt.

Das Problem: Ingenieure müssen diese Regeln mühsam von Hand schreiben. Das ist wie wenn Sie jeden einzelnen Stein in einem 100-stöckigen Gebäude einzeln mit einem Lineal vermessen müssten. Es dauert ewig und ist fehleranfällig.

Künstliche Intelligenz (KI) könnte helfen, aber bisher waren die KIs zu „dumm" für diese spezielle Aufgabe. Sie waren wie Generalisten, die alles können, aber nichts wirklich perfekt beherrschen. Wenn man sie fragte: „Baue eine Regel, damit das Licht angeht, wenn der Schalter gedrückt wird", antworteten sie oft mit Unsinn oder falscher Syntax, weil ihnen das tiefe Verständnis für die Bausteine fehlte.

Hier kommt das Papier QiMeng-CodeV-SVA ins Spiel. Die Forscher haben eine clevere Methode entwickelt, um eine spezialisierte KI zu trainieren. Man kann sich das in drei Schritten vorstellen:

1. Der riesige Bauplan-Schatz (RTL-Grounded Synthesis)

Statt nur ein paar alte Lehrbuchbeispiele zu nutzen (was wie das Lernen aus einem verstaubten Wörterbuch wäre), haben die Forscher einen riesigen Berg an echten, offenen Bauplänen (RTL-Code) gesammelt.

• Die Analogie: Stellen Sie sich vor, Sie wollen einen Kochkurs für „echte Gerichte" geben. Statt nur Rezepte aus einem alten Buch zu nehmen, gehen Sie in eine riesige Küche, wo tausende echte Gerichte zubereitet werden. Sie lassen eine KI diese Gerichte beobachten und dann beschreiben: „Was passiert hier? Wenn das Wasser kocht, muss der Deckel drauf."
• Die KI hat also Millionen von echten Schaltungen analysiert und daraus automatisch Sicherheitsregeln abgeleitet. Das hat den Datensatz von winzigen 4.000 Beispielen auf über 100.000 erweitert.

2. Der Spiegel-Test (Bidirectional Data Synthesis)

Das war der genialste Trick. Eine KI kann manchmal lügen oder Dinge missverstehen. Wie erkennt man das?

• Die Analogie: Stellen Sie sich vor, Sie geben einer KI eine Regel auf Deutsch: „Das Licht geht an, wenn der Schalter gedrückt wird." Die KI schreibt eine Regel in der strengen SVA-Sprache.
  • Jetzt nehmen wir diese SVA-Regel und geben sie einer anderen KI (oder derselben) zurück, mit der Aufgabe: „Erkläre mir diese Regel wieder auf Deutsch."
  • Wenn die KI zurück auf Deutsch sagt: „Das Licht geht an, wenn der Schalter gedrückt wird", dann war die Übersetzung korrekt.
  • Wenn sie aber sagt: „Das Licht geht an, wenn der Schalter los gelassen wird", dann hat die KI einen Fehler gemacht.
• Die Forscher haben diesen „Hin-und-Her-Test" (Bidirectional Translation) millionenfach durchgeführt. Nur die Paare, die sich am Ende genau entsprachen, wurden als „wahr" und gut für das Training ausgewählt. Das hat viele schlechte Beispiele aussortiert, die sogar von formellen Prüfprogrammen als „korrekt" durchgewunken wurden, aber inhaltlich Unsinn waren.

3. Der Spezialist entsteht (Training)

Mit diesem riesigen, sauberen Datensatz haben sie eine KI (basierend auf dem Modell Qwen) trainiert.

• Das Ergebnis: Diese neue KI, CodeV-SVA, ist wie ein Meister-Handwerker, der nur für Sicherheitsregeln ausgebildet wurde.
• Sie ist nicht nur schneller, sondern auch genauer als die teuersten, allgemeinen KI-Modelle (wie GPT-5 oder DeepSeek-R1), die man sonst kaufen müsste.
• In Tests schaffte sie es, in über 75% der Fälle die perfekte Regel auf Anhieb zu schreiben, während die großen, allgemeinen KIs oft nur bei 60-70% lagen.

Warum ist das wichtig?

Früher musste man für diese Aufgabe riesige, teure KI-Modelle mieten oder Jahre an Daten sammeln. Jetzt haben die Forscher gezeigt, dass man mit einer cleveren Methode (dem Spiegel-Test und echten Bauplänen) eine kleine, spezialisierte KI bauen kann, die besser ist als die Riesen.

Zusammengefasst:
Die Forscher haben eine KI nicht einfach nur mit mehr Daten gefüttert, sondern ihr beigebracht, sich selbst zu überprüfen. Sie haben aus einem Berg roher Baupläne eine Bibliothek perfekter Sicherheitsregeln gezaubert. Das Ergebnis ist ein digitaler Sicherheitsinspektor, der billiger, schneller und genauer ist als alles, was es vorher gab. Das bedeutet sicherere Computerchips für unsere Smartphones, Autos und Server – und das alles dank einer KI, die gelernt hat, nicht nur zu reden, sondern auch zu verstehen.

Technische Zusammenfassung

1. Problemstellung

Die hardwarebasierte formale Verifikation ist ein entscheidender Schritt im digitalen Entwurfsprozess. Dabei müssen Ingenieure basierend auf natürlichen Sprachspezifikationen und Register-Transfer-Level (RTL)-Code temporale logische Aussagen formulieren, sogenannte SystemVerilog Assertions (SVAs).
Das Hauptproblem liegt in der hohen manuellen Arbeitsbelastung und der benötigten Expertise für die Erstellung hochwertiger SVAs. Zwar versuchen aktuelle Ansätze, allgemeine Large Language Models (LLMs) für die Übersetzung von natürlicher Sprache zu SVA (NL2SVA) einzusetzen, doch diese zeigen erhebliche Schwächen:

• Datenmangel: Es gibt einen Mangel an hochwertigen, realweltlichen SVA-Korpora. Öffentliche Datensätze sind oft klein oder stammen aus Lehrbüchern.
• Semantische Äquivalenz: Es fehlt an zuverlässigen Methoden, um zu prüfen, ob eine generierte SVA semantisch korrekt mit der natürlichen Sprachbeschreibung übereinstimmt.
• Fehleranfälligkeit: Allgemeine LLMs (wie DeepSeek-V3.1 oder GPT-5) scheitern oft an der spezifischen Syntax und Semantik von SVAs oder erzeugen triviale Aussagen (z. B. assert property (1'b1)), die zwar formal verifizierbar sind, aber keine echte Prüfung darstellen.
• Kosten: Hochleistungs-LLMs sind teuer in der Bereitstellung und erfüllen oft nicht die proprietären Anforderungen von Hardware-Firmen.

2. Methodik: Der CodeV-SVA Ansatz

Die Autoren stellen einen effizienten Rahmen zur Datensynthese und zum Training spezialisierter Modelle vor, der in vier Hauptphasen unterteilt ist:

A. SVA-Synthese aus realen RTL-Code (RTL-Grounded Synthesis)

Um das Datenproblem zu lösen, nutzen die Autoren große Mengen an Open-Source-RTL-Code (aus dem CodeV-Datensatz) als Design-Under-Test (DUT).

1. Ein allgemeines LLM (DeepSeek-V3.1) analysiert den RTL-Code und generiert dazu passende natürliche Sprach-Eigenschaften (NL Properties) und entsprechende SVAs.
2. Ein formales Verifikationswerkzeug (JasperGold) filtert die generierten SVAs und behält nur diejenigen bei, die unter dem gegebenen RTL-Code formal verifiziert werden können. Dies ergibt einen Seed-Datensatz von 159.000 Instanzen.

B. Bidirektionale Selektion (Bidirectional Data Selection)

Dies ist der Kerninnovation zur Sicherstellung der semantischen Qualität. Da eine formal verifizierte SVA nicht zwingend die volle Semantik der natürlichen Sprache abbildet, wird ein „Hin-und-Her"-Übersetzungsprozess angewendet:

1. SVA zu NL: Die generierte SVA wird zurück in eine natürliche Sprachbeschreibung übersetzt.
2. NL zu SVA: Diese neue Beschreibung wird erneut in eine SVA übersetzt.
3. Äquivalenzprüfung: Die neu generierte SVA wird formal auf logische Äquivalenz mit der ursprünglichen SVA geprüft. Nur Paare, die diese Prüfung bestehen, werden behalten.

• Ergebnis: Dieser Prozess eliminiert subtile Fehler (z. B. Operator-Präzedenzprobleme), die von Verifikationswerkzeugen oder „LLM-as-a-judge" übersehen werden, und reduziert den Datensatz auf 105.000 hochqualitative Paare.

C. Weitere Qualitätsverbesserung (Refinement)

Zusätzliche Filterungsschritte erhöhen die Effizienz und Genauigkeit:

• LLM-as-a-Judge mit Expertenwissen: Fehlerkategorien (logische Fehlausrichtung, Signalinkonsistenz etc.) werden definiert und ein LLM filtert diese heraus.
• Schwierigkeitsfilterung: Ein schwächeres Modell (Qwen3-8B) wird genutzt, um triviale Datenpunkte zu entfernen, die es leicht lösen kann.
• Reasoning Augmentation: Ein starkes Reasoning-Modell (DeepSeek-R1) fügt dem Datensatz lange Denkpfade (Reasoning Trajectories) hinzu, um das Modell beim logischen Schlussfolgern zu trainieren.

D. Supervised Fine-Tuning (SFT)

Auf Basis des bereinigten Datensatzes (83.000 Instanzen) werden Open-Source-Modelle (Qwen3-8B und Qwen3-14B) mittels SFT feinabgestimmt, um CodeV-SVA zu erhalten. Das Training nutzt das Format von DeepSeek-R1, bei dem der Reasoning-Pfad zwischen speziellen Tokens platziert wird.

3. Wichtige Beiträge

• Neuer Datensatz-Paradigmen: Statt auf existierende, oft unzureichende SVA-Datenbanken zu setzen, wird ein Framework zur Synthese von SVA-Daten direkt aus massivem Open-Source-RTL-Code vorgestellt.
• Bidirektionale Validierung: Einführung einer robusten Methode zur automatischen Überprüfung der semantischen Äquivalenz zwischen natürlicher Sprache und SVA durch zyklische Übersetzung und formale Verifikation.
• Spezialisierte Modelle: Entwicklung von CodeV-SVA-8B und CodeV-SVA-14B, die speziell für die Hardware-Verifikation trainiert wurden und dabei deutlich kosteneffizienter sind als proprietäre Modelle.
• Open Source: Die Autoren planen, den gesamten Datensatz, die Modelle und die Trainingspipeline zu veröffentlichen.

4. Ergebnisse

Die Modelle wurden auf dem Benchmark FVEval-NL2SVA (mit den Teilaufgaben Human und Machine) evaluiert. Die Metrik ist die funktionale Korrektheit (Func.@k), d. h., ob die generierte SVA logisch äquivalent zur Ground-Truth ist.

• Leistungsführerschaft: CodeV-SVA-14B erreicht 75,8% (Func.@1) auf dem NL2SVA-Human-Benchmark und 84,0% auf dem NL2SVA-Machine-Benchmark.
• Vergleich mit State-of-the-Art: Diese Ergebnisse übertreffen oder entsprechen den besten allgemeinen LLMs wie GPT-5 und DeepSeek-R1 (671B), obwohl CodeV-SVA-14B nur ein Bruchteil der Parametergröße hat.
• Steigerung gegenüber Basismodellen: Im Vergleich zum Basismodell Qwen3-14B (61,6% auf Human) zeigt sich eine massive Verbesserung durch die spezialisierte Datensynthese.
• End-to-End-Verifikation: In einem automatisierten Verifikationsworkflow (basierend auf AssertionForge) generierte CodeV-SVA-8B signifikant mehr syntaktisch korrekte und verifizierbare SVAs als GPT-4o oder DeepSeek-R1 (z. B. 2,5-fach mehr verifizierte SVAs beim komplexen Design OPENMSP430).

5. Bedeutung

Das Paper demonstriert, dass die Kombination aus RTL-gegründeter Datensynthese und bidirektionaler Validierung ein effektiver Weg ist, um hochwertige Trainingsdaten für spezialisierte Domänen-LLMs zu erzeugen.

• Es löst das Problem des Mangels an realen SVA-Daten.
• Es bietet eine kosteneffiziente Alternative zu teuren proprietären Modellen für die Hardware-Verifikation.
• Es zeigt, dass spezialisierte, kleinere Modelle durch hochwertige Daten und Reasoning-Training die Leistung riesiger allgemeiner Modelle in Nischenbereichen übertreffen können.

Dieser Ansatz ebnet den Weg für eine breitere Automatisierung der Hardware-Verifikation und reduziert die Abhängigkeit von manueller Expertenarbeit.