🤖 AI

SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation

Dieser Beitrag stellt SpecAlign vor, ein Framework, das die semantische Ausrichtung von von LLMs generierten SystemVerilog-Assertions mit natürlichen Sprachspezifikationen durch eine iterative, auf Implikation basierende Evaluierung, Chain-of-Thought-Argumentation und Selbstkonsistenz-Stimmabgabe verbessert und dadurch die Genauigkeit der Assertions ohne Rückgriff auf goldenes RTL steigert.

Ursprüngliche Autoren: Jaime Rafael Imperial, Hao Zheng

Veröffentlicht 2026-05-26

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Jaime Rafael Imperial, Hao Zheng

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 sind ein Meisterarchitekt (die Design-Spezifikation), der detaillierte Baupläne für ein neues, komplexes Haus entworfen hat. Sie möchten einen sehr schnellen, sehr kreativen, aber gelegentlich verträumten Bauleiter (das Large Language Model oder LLM) einstellen, um eine Liste von Sicherheitsregeln für das Haus zu verfassen. Diese Regeln sind in einem strengen, technischen Code namens SystemVerilog Assertions (SVA) geschrieben.

Das Problem? Der Bauleiter ist hervorragend darin, Sätze zu schreiben, die wie Sicherheitsregeln aussehen und den Grammatiktest bestehen, aber manchmal sind die von ihm geschriebenen Regeln tatsächlich Unsinn oder widersprechen Ihren ursprünglichen Bauplänen.

Zum Beispiel besagt Ihr Bauplan: „Die Vordertür muss sich verriegeln, wenn der Alarm aktiv ist." Der Bauleiter könnte eine Regel schreiben, die lautet: „Die Vordertür muss sich verriegeln, wenn die Vordertür aktiv ist." Es klingt wie eine Regel, und ein Computer könnte sogar sagen: „Ja, das ist ein gültiger Satz", aber in der realen Welt ergibt das keinen Sinn.

Das Problem: „Gültig", aber falsch

Traditionell prüften Ingenieure, ob diese Regeln gut sind, indem sie ein physisches Modell des Hauses (das sogenannte Golden RTL) bauten und die Regeln daran testeten. Wenn die Regel das Modell nicht brach, gingen sie davon aus, dass sie gut war.

Aber das Papier argumentiert, dass dies so ist, als würde man prüfen, ob eine Regel funktioniert, indem man nur sieht, ob sie in ein bestimmtes Modell passt. Wenn das Modell perfekt ist, großartig. Aber was, wenn Sie das Modell noch nicht haben? Oder was, wenn die Regel technisch „wahr" für dieses spezifische Modell ist, aber den Punkt dessen, was Sie verlangt haben, völlig verfehlt? Der Bauleiter könnte Regeln halluzinieren, die intelligent klingen, aber nutzlos sind.

Die Lösung: SpecAlign

Die Autoren stellen SpecAlign vor, ein neues „Qualitätskontroll"-Rahmenwerk. Anstatt ein physisches Modell zu bauen, um die Regeln zu testen, fungiert SpecAlign wie ein superkluger Übersetzer und Faktenprüfer, der die Regeln des Bauleiters direkt mit Ihren ursprünglichen Bauplänen (den Spezifikationen in natürlicher Sprache) vergleicht.

So funktioniert SpecAlign, anhand einer einfachen Analogie:

1. Der Übersetzungsschritt (Normalisierung)

Der Bauleiter schreibt Regeln in einem strengen Code (SVA). SpecAlign übersetzt diese zunächst zurück in einfaches Englisch.

Analogie: Stellen Sie sich vor, der Bauleiter schreibt in „Baustellencode". SpecAlign übersetzt ihn zurück ins „Englische", damit er direkt mit Ihren englischen Bauplänen verglichen werden kann.

2. Der zweistufige Faktencheck (Ausrichtungs-Schleifen)

SpecAlign führt zwei Runden der Prüfung durch:

Runde 1 (Eigenschaftsprüfung): Es prüft die Ideen, die der Bauleiter aus Ihren Bauplänen extrahiert hat. Stimmen diese Ideen mit dem überein, was Sie geschrieben haben?
Runde 2 (Regelprüfung): Es prüft die tatsächlich übersetzten Regeln. Stimmen sie mit den Ideen und Ihren Bauplänen überein?

3. Das „Drei-Fächer"-Urteil

Anstatt nur „Bestanden" oder „Durchgefallen" zu sagen, sortiert SpecAlign jede Regel in eines von drei Fächern ein:

🟢 Folgt (Grün): Die Regel stimmt perfekt mit Ihren Bauplänen überein. „Ja, das ist genau das, was Sie verlangt haben."
🔴 Widerspricht (Rot): Die Regel kämpft direkt gegen Ihre Baupläne. „Nein, Sie sagten, die Tür verriegelt sich bei Alarm, aber diese Regel sagt, sie entriegelt sich."
⚪ Unbekannt (Grau): Die Regel erwähnt Dinge, über die Ihre Baupläne nie gesprochen haben. „Sie haben ein 'Smart-Lock' erwähnt, aber Ihre Baupläne sagten nur 'Tür'. Ich weiß nicht, ob dieses zusätzliche Feature in Ordnung ist oder nicht."

4. Die „Selbstkorrektur"-Schleife

Wenn eine Regel im Roten (Widerspricht) Fach landet, wirft SpecAlign sie nicht einfach weg. Es fungiert wie ein strenger Redakteur:

Es teilt dem Bauleiter genau mit, wo die Regel falsch lag.
Es bittet den Bauleiter, die Regel basierend auf den Bauplänen neu zu schreiben.
Es prüft die neue Regel erneut.
Es wiederholt dies, bis die Regel Grün ist oder zumindest eindeutig Grau.

Um sicherzustellen, dass der „Redakteur" keine Fehler macht, bittet SpecAlign die KI, das Problem auf drei verschiedene Arten durchzudenken (wie beim Befragen von drei verschiedenen Experten) und stimmt dann über die endgültige Antwort ab. Dies wird Selbstkonsistenz genannt.

Die Ergebnisse: Aufräumen im Chaos

Die Autoren testeten dies an zwei realen Designs (wie Kommunikationsprotokolle für Chips, ähnlich wie ein USB- oder Netzwerkkarte mit einem Computer spricht).

Vor SpecAlign: Eine konkurrierende Methode generierte Hunderte von Regeln. Die meisten waren entweder Rot (widersprachen den Bauplänen) oder Grau (erfanden Details). Nur ein winziger Bruchteil war Grün (entsprach tatsächlich den Bauplänen).
Nach SpecAlign:
- Die Anzahl der Roten (widersprechenden) Regeln sank dramatisch. Für ein Design gingen sie von 148 schlechten Regeln auf nur noch 6 zurück.
- Die Anzahl der Grünen (ausgerichteten) Regeln stieg signifikant.
- Die Anzahl der Grauen (Unbekannten) Regeln stieg. Warum? Weil SpecAlign aufhörte, so zu tun, als wären Regeln mit erfundenen Details „gut". Es identifizierte sie korrekt als „wir haben nicht genug Informationen, um zu sagen, dass dies gut ist".

Die große Erkenntnis

Das Papier kommt zu dem Schluss, dass nur weil eine Regel grammatikalisch korrekt ist oder einen Computertest besteht, nicht bedeutet, dass sie das bedeutet, was Sie denken, dass sie bedeutet.

SpecAlign bietet eine Möglichkeit zu prüfen, ob die KI tatsächlich Ihren Anweisungen folgt, ohne dass zuerst ein physisches Modell gebaut werden muss. Es verwandelt einen Haufen „technisch gültiger, aber nutzloser" Regeln in einen kleineren, saubereren Satz von Regeln, denen Sie tatsächlich vertrauen können, und markiert gleichzeitig diejenigen, die zu vage sind, um sich sicher zu sein.

Technische Zusammenfassung: SpecAlign – Ein semantisches Ausrichtungsframework für die Generierung von SystemVerilog-Assertions

1. Problemstellung

Die zunehmende Komplexität moderner Hardware-Designs hat die Einführung von Large Language Models (LLMs) zur Generierung von SystemVerilog-Assertions (SVA) zur Unterstützung der assertionsbasierten Verifikation (ABV) vorangetrieben. Die bestehenden LLM-Ansätze konzentrieren sich jedoch primär auf die syntaktische Korrektheit und die Ergebnisse der formalen Verifikation (FV) (z. B. ob eine Assertion bewiesen wird oder auf einem gegebenen RTL eine Gegenbeispiel liefert). Diese Metriken adressieren die semantische Ausrichtung nicht: Ob die generierte Assertion die in der natürlichen Spezifikation beschriebene Verhaltensabsicht genau widerspiegelt.

LLMs können Assertions produzieren, die syntaktisch korrekt und auf einer spezifischen RTL-Implementierung formal beweisbar sind, aber semantisch wirkungslos oder halluziniert sind. Beispielsweise könnte eine Assertion einen Takt an derselben Flanke abtasten, die die Eigenschaft auslöst, wodurch sie trotz Bestehens der FV trivial (vacuous) wird. In Abwesenheit eines „goldenen" RTL-Modells zum Vergleich ist die manuelle Überprüfung solcher Assertions zeitaufwendig und verringert das Vertrauen. Darüber hinaus sehen sich FV-Engines bei der Bewertung großer Mengen generierter Assertions für komplexe Designs mit Skalierungsproblemen (Zustandsraumexplosion) konfrontiert. Es besteht ein kritischer Bedarf an einem Framework, das die semantische Konsistenz gegenüber der Spezifikation selbst bewertet, unabhängig von RTL-Implementierungsdetails.

2. Methodik: Das SpecAlign-Framework

SpecAlign ist ein spezifikationszentriertes Framework, das entwickelt wurde, um von LLMs generierte SVAs zu bewerten und iterativ zu verfeinern, ohne auf ein goldenes RTL zurückzugreifen. Es arbeitet durch zwei primäre iterative Schleifen: eine Property-Ausrichtungsschleife und eine SVA-Ausrichtungsschleife. Beide Schleifen nutzen drei Kernphasen: Ausrichtungsprüfung, Inkonsistenzanalyse und Evidenzextraktion.

A. Architekturübersicht

Das Framework normalisiert den Vergleich zwischen verschiedenen Darstellungen der Designabsicht. Während die Eingabe aus natürlichen Spracheigenschaften ( $P$ ) und generierten SVAs ( $A$ ) besteht, wandelt das Framework jede SVA über einen spezifischen Extraktionsprozess in eine Zusammenfassung in natürlicher Sprache ( $N$ ) um. Diese Normalisierung ermöglicht es, sowohl Eigenschaften als auch Assertions auf derselben semantischen Ebene gegenüber der Designspezifikation ( $S$ ) zu bewerten.

B. Kernkomponenten

Ausrichtungsprüfung:
- Klassifizierung: Das Framework klassifiziert Beschreibungen in natürlicher Sprache ( $X_i$ $X_{i}$ ) basierend auf ihrer Beziehung zur Spezifikation in drei Kategorien:
  - Impliziert (Entails): Alle Elemente werden durch die Spezifikation gestützt.
  - Widerspricht (Contradicts): Mindestens ein Element widerspricht der Spezifikation.
  - Unbekannt (Unknown): Elemente werden weder gestützt noch widerlegt (oft aufgrund von implementierungsspezifischen Annahmen, die nicht in der Spezifikation enthalten sind).
- Selbstkonsistenz-Abstimmung: Um die Zuverlässigkeit zu erhöhen, verwendet das System eine Chain-of-Thought (CoT)-Prompting-Strategie. Es generiert $k$ Denkpfade für eine gegebene Eingabe und aggregiert die Teilurteile mittels Mehrheitsentscheid. Im Falle eines Unentschiedens wird eine konservative Priorität angewendet: Widerspricht > Unbekannt > Impliziert.
- Referenzselektion: Die Property-Schleife verwendet die Designspezifikation ( $S$ ) als Referenz. Die SVA-Schleife verwendet eine „Ausgerichtete Eigenschaftsbank" (falls verfügbar), um Rauschen aus verstreuten Spezifikationsdokumenten zu reduzieren; andernfalls greift sie auf $S$ zurück.
Inkonsistenzanalyse und Verfeinerung:
- Wenn ein Urteil Widerspricht lautet, führt das System eine Inkonsistenzanalyse durch. Es identifiziert die spezifischen konfligierenden Elemente in der Beschreibung, verweist auf das korrekte Verhalten in der Spezifikation und generiert strukturiertes, handlungsorientiertes Feedback ( $F_i$ ).
- Dieses Feedback leitet das LLM an, die Eigenschaft oder Assertion ( $P'_i$ oder $A'_i$ ) neu zu generieren, indem es Auslösebedingungen explizit definiert und die Einführung neuer Signale oder Verhaltensweisen vermeidet, die nicht in der Spezifikation enthalten sind.
- Die verfeinerte Ausgabe wird in der Ausrichtungsschleife erneut bewertet, bis eine feste Anzahl von Iterationen erreicht ist oder die Ausgabe ausgerichtet ist.
Evidenzextraktion:
- Für Fälle, die Impliziert sind, extrahiert das System stützende Evidenz (Zitate und Stellen) aus der Spezifikation, um die manuelle Überprüfung zu erleichtern und das Vertrauen zu stärken.
- Für Fälle, die Unbekannt sind, kategorisiert das System, welche Elemente mehrdeutig oder undefiniert sind, und unterscheidet echte Widersprüche von unzureichend spezifiziertem Verhalten.
Quantitative Metrik:
- Das Framework definiert einen Ausrichtungs-Score ( $a_t$ ), der als Verhältnis der implizierten Assertions ( $E$ ) zur Gesamtzahl der Assertions ( $n$ ) in einer gegebenen Iteration berechnet wird ( $a_t = E/n$ ). Das Ziel des Verfeinerungsprozesses ist es, diesen Score zu maximieren.

C. Extraktion von Zusammenfassungen in natürlicher Sprache

Ein kritischer Vorverarbeitungsschritt besteht darin, formale SVAs in strukturierte Zusammenfassungen in natürlicher Sprache umzuwandeln. Das LLM wird aufgefordert, spezifische SVA-Komponenten (Trigger, Antezedens, Implikationsoperator, Konsequens und Disable If) zu identifizieren und sie auf äquivalente Phrasen in natürlicher Sprache abzubilden. Dies stellt sicher, dass die semantische Absicht des formalen Codes für den Vergleich erhalten bleibt.

3. Hauptbeiträge

Der Artikel skizziert folgende Beiträge:

Semantisches Evaluierungs-Framework: Ein neuartiger Ansatz zur Bewertung von LLM-generierten SVAs gegenüber Spezifikationen in natürlicher Sprache, ohne auf formale Verifikation angewendet auf goldenes RTL zurückzugreifen.
Iterativer Verfeinerungspipeline: Ein strukturiertes Framework bestehend aus Ausrichtungsprüfung, Inkonsistenzanalyse und SVA-Zusammenfassungsextraktion, das für die Integration in bestehende LLM-basierte Generierungsworkflows konzipiert ist.
Quantitative Ausrichtungs-Metrik: Eine Ausrichtungs-Score-Metrik basierend auf der Klassifizierung semantischer Implikation zur Messung der Spezifikationskonsistenz, die eine skalierbare Alternative zur traditionellen FV-Korrektheitsbewertung bietet.
Inkonsistenz-Analyse-Mechanismus: Eine Methode zur Generierung spezifischen, handlungsorientierten Feedbacks für widersprüchliche Eigenschaften und Assertions, die sowohl die manuelle Überprüfung als auch die automatische Verfeinerung unterstützt.
Empirische Validierung: Experimentelle Ergebnisse, die die Reduktion widersprüchlicher Assertions in APB- und UART-Designs durch semantische Verfeinerung demonstrieren.

4. Experimentelle Ergebnisse

Die Autoren bewerteten SpecAlign an zwei Hardware-Designs: APB (APB zu I2C-Schnittstelle) und UART (UART zu Bus-Schnittstelle). Das Framework wurde mit AssertionForge verglichen, einer Baseline-Methode, die einen Wissensgraphen verwendet und RTL in die Generierung einbezieht.

APB-Ergebnisse:
- Baseline (AssertionForge): Generierte 442 SVAs mit einem Ausrichtungs-Score von 0,02. Nur 8 wurden als impliziert eingestuft, während 148 widersprüchlich waren.
- SpecAlign: Behielt 442 SVAs bei, erhöhte jedoch den Ausrichtungs-Score auf 0,15. Entscheidend sank die Anzahl der widersprüchlichen Assertions auf 0, wobei 66 Assertions als impliziert eingestuft wurden. Die verbleibenden 376 wurden als Unbekannt klassifiziert.
UART-Ergebnisse:
- Baseline: Generierte 325 SVAs mit einem Ausrichtungs-Score von 0,06 (21 impliziert, 142 widersprüchlich).
- SpecAlign: Generierte 319 SVAs mit einem Ausrichtungs-Score von 0,28. Widersprüchliche Assertions wurden auf 6 reduziert, während implizierte Assertions auf 92 anstiegen.

Analyse der Ergebnisse:
Die Experimente zeigten, dass Baseline-Methoden oft Assertions generieren, die entweder der Spezifikation widersprechen oder stark auf implementierungsspezifischen Details (RTL) beruhen, die nicht in der Spezifikation in natürlicher Sprache zu finden sind. SpecAlign filtert diese Widersprüche effektiv heraus. Die Zunahme der „Unbekannt"-Klassifizierungen bei SpecAlign (z. B. 376 für APB) wird nicht als Versagen interpretiert, sondern als eine konservativere und genauere Klassifizierungsstrategie, die implementierungsspezifische Annahmen von durch die Spezifikation gestütztem Verhalten trennt. Diese Unterscheidung verhindert die falsche positive Kennzeichnung von nicht unterstütztem Verhalten als „impliziert".

5. Bedeutung und Behauptungen

Der Artikel behauptet, dass SpecAlign eine skalierbare Ergänzung zur traditionellen formalen Verifikation darstellt. Durch die Trennung der semantischen Korrektheit von RTL-Beweisergebnissen adressiert es die Einschränkung, dass die formale Verifikation allein nicht bestimmen kann, ob eine Assertion das in der Spezifikation beschriebene beabsichtigte Verhalten erfasst.

Die Autoren betonen, dass die formale Verifikation zwar notwendig ist, um zu beweisen, dass Assertions auf RTL gelten, aber unzureichend ist, um die Qualität der Absicht der Assertion zu bewerten. SpecAlign verbessert das Vertrauen in von LLMs generierte Assertions durch:

Die Erkennung semantischer Inkonsistenzen, die formale Tools möglicherweise übersehen (z. B. triviale Wahrheiten).
Die Reduzierung des Debug-Aufwands durch die Identifizierung von Widersprüchen vor der RTL-Simulation oder dem formalen Beweis.
Die Bereitstellung eines Mechanismus zur iterativen Verfeinerung von Assertions ohne Anforderung eines goldenen Modells.

Der Artikel schließt bescheiden, indem er feststellt, dass das Framework zwar die Ausrichtung verbessert, aber zukünftige Arbeiten erforderlich sind, um Klassifizierungsmethoden zu verfeinern, syntaktische Fehler besser zu erfassen und den Ansatz auf andere Aufgaben der Hardware-Design-Automatisierung wie RTL-Generierung und Debugging auszudehnen.