TensorEQC: Structure-Aware Equivalence Checking with GF(2) Algebra, Exact Tensor Networks, and Reset Analysis : a Multi-Algorithmic Study of Datapath Verification and Reset-State Dependence

Technische Zusammenfassung: TensorEQC – Struktur-bewusste Äquivalenzprüfung

Problemstellung
Die Äquivalenzprüfung (Equivalence Checking, EC) reagiert hochsensibel auf die Repräsentation eines Schaltungsteils. Unterschiedliche Schaltungsstrukturen – wie etwa XOR-reiche Netzwerke, Carry-Chains, Endlichkeitskörper-Multiplizierer und Integer-Multiplizierer – weisen distinkte strukturelle Eigenschaften auf, die unterschiedliche Verifizierungsansätze begünstigen. Keine einzelne Methode (z. B. Boole’sche Algebra, Entscheidungsdiagramme oder Tensornetzwerke) dominiert universell alle Schaltungstypen. Darüber hinaus erfordert die Verifizierung sequentieller Schaltungen die Unterscheidung zwischen beobachtbarer Abhängigkeit vom Initialzustand und Unsicherheit, die sich innerhalb einer spezifischen Beobachtungsgrenze auflöst, insbesondere im Hinblick auf Reset-Zustände.

Methodik
Das Paper führt TensorEQC ein, einen ausführbaren Forschungs-Workflow, der als multi-algorithmisches Portfolio und nicht als monolithischer Einzel-Solver konzipiert ist. Die Kernphilosophie besteht darin, dass eine Engine eine Verifizierungspflicht nur dann entlasten sollte, wenn sie dies gemäß ihrer eigenen exakten Semantik tun kann; andernfalls wird die Pflicht an eine andere Engine übergeben.

Der Workflow besteht aus drei primären Komponenten:

1. Kombinatorisches Portfolio: Eine sequentielle Pipeline von Verifizierungs-Engines, die Ausgaben verarbeitet, bis diese entweder entlastet sind oder ein Ressourcenlimit erreicht wird. Die Pipeline umfasst:
   • Strukturelles Hashing: Etabliert die Identität von Ausdrucks-DAGs unter unterstützten Primitiven (AND, OR, XOR usw.) mittels kommutativer Normalisierung.
   • Simulation: Verwendet Packed Simulation mit Zufalls-, All-Zero- und All-One-Mustern, um negative Zeugen (Gegenbeispiele) zu finden.
   • Algebraische Normalformen (ANF): Repräsentiert Boole'sche Funktionen als multilineare Polynome über GF(2). Es nutzt ein spezifisches Lemma, um exakte negative Zeugen aus nicht-null Polynomen zu generieren.
   • Relationale Tensor-Elimination: Repräsentiert Gates als Boole'sche Indikator-Tensoren. Sie führt die Variablenelimination mittels Disjunktion über den Boole'schen Semiring durch (um die Existenz erfüllender Zuweisungen zu bewahren), anstatt über GF(2)-Summation (welche die Parität berechnet).
   • ROBDD & Exhaustive Fallback: Verwendet Ordered Binary Decision Diagrams mit Node-Caps und Exhaustive Enumeration mit geringer Unterstützung als finale Fallbacks.
2. Tensor Train (TT) Analytik: Ein Begleitmodul, das exakte TT-Repräsentationen aus Wahrheitstabellen konstruiert, um den algebraischen Rang zu messen und auf Null-Funktionen zu testen. Es unterscheidet zwischen Rängen über GF(2) und reellen Zahlen und stellt fest, dass GF(2)-Ränge signifikant kleiner sein können.
3. Reset-Analyse: Ein synchrones Modul, das mittels expliziter Zustands-Selbstkomposition prüft, ob eine Abhängigkeit vom Initialzustand vorliegt. Es unterscheidet zwischen Fällen, in denen die Reset-Abhängigkeit sofort beobachtbar ist, und Fällen, in denen sie nach einer spezifischen Anzahl von „Flushing“-Zyklen verschwindet.

Wesentliche Beiträge

• Integration exakter Engines: Die Arbeit demonstriert eine praktische Integration von strukturellem Hashing, GF(2)-Algebra, relationalen Tensornetzwerken und ROBDDs, wobei die distinkten Beweisverträge (Proof Contracts) für jede Engine gewahrt bleiben.
• Struktur-bewusste Strategie: Sie liefert empirische Belege dafür, dass die Effizienz der Verifizierung stark von der Schaltungsstruktur und der Variablenordnung abhängt. Beispielsweise ergeben verschachtelte Addierer-Operanden niedrige Tensor-Ränge (≤3), während getrennte Operanden hohe Ränge (129) zur Folge haben, was letztere weniger geeignet für Tensor-basierte Ansätze macht.
• Reset-Zustands-Diagnostik: Sie bietet eine Methode, um explizit zwischen echter Initialzustands-Abhängigkeit und transienter Unsicherheit in synchronen Designs zu unterscheiden.
• Reproduzierbare Validierung: Das Paper enthält ein neues, in sich geschlossenes Supplement, das die exakte GF(2) Tensor-Train-Konstruktion, Rangmessungen und Null-Funktions-Tests an fünf 16-Input-Funktionen validiert und somit die Unterscheidung zwischen Paritäts-Auslöschung und tatsächlichen Null-Funktionen bestätigt.

Experimentelle Ergebnisse
Die Studie berichtet über zwei unterschiedliche Datensätze:

1. Historische Portfolio-Kampagne (v1.0.0): Dieser Datensatz umfasst 89 Testläufe mit 2.048-Bit Ripple-Addierern, 128-Bit Polynomial-Basis-Multiplizierern und affinen Netzwerken.
   • Erfolge: Der vollständige Flow verifizierte erfolgreich 2.048-Bit Ripple-Addierer (2,87s) und 128-Bit GF-Multiplizierer (0,80s) und übertraf damit in spezifischen Fällen BDD-basierte Ansätze (z. B. bei 2.048-Bit Addierern, bei denen BDDs scheiterten).
   • Limitierungen: Der Ansatz stieß bei 1.024-Bit Ripple-Addierern und 1.024-Input affinen Netzwerken an Ressourcenlimits (Node Caps, Width Caps). Die Ergebnisse für Integer-Multiplikation waren aufgrund des ANF-Wachstums und der Tensor-Scope-Caps auf 10 Bit begrenzt.
   • Beobachtung: Der vollständige Flow verursachte teilweise Overheads im Vergleich zur direkten Auswahl der optimalen Engine, was den Trade-off zwischen Automatisierung und Effizienz verdeutlicht.
2. Neues Reproduzierbares Supplement: Ein fokussiertes Experiment an fünf 16-Input-Funktionen (einschließlich Parität und GF-Multiplikation) bestätigte, dass die exakte Tensor-Train-Konstruktion und Ranganalyse für kleine Funktionen machbar sind. Es validierte, dass eine skalare GF(2)-Summe von Null nicht eine Null-Funktion impliziert (Paritätsauslöschung), eine Unterscheidung, die durch den TT Zero-Test korrekt gehandhabt wurde.

Bedeutung und Ansprüche
Das Paper rahmt seinen Beitrag explizit als gezielte technische Bewertung (Scoped Technical Assessment) und nicht als universelle Lösung ein.

• Keine universelle Überlegenheit: Die Ergebnisse stützen nicht die Behauptung, dass Tensornetzwerke allen anderen Methoden überlegen sind. Stattdessen unterstützen sie eine „repräsentationssensitive Strategie“, bei der verschiedene Engines basierend auf dem mathematischen Bereich (z. B. GF-Algebra für Funktionen mit niedrigem Grad im endlichen Körper, relationale Elimination für Carry-Chains) ausgewählt werden.
• Integration statt Ersatz: Das zentrale Ergebnis ist die erfolgreiche Integration von exakter Algebra, relationaler Elimination, Entscheidungsdiagrammen und zeitlicher Logik unter Wahrung der jeweils distinkten Beweisverträge.
• Explizite Grenzen: Der Autor betont, dass die aktuelle Implementierung auf binäre kombinatorische Primitive und kleine synchrone Maschinen beschränkt ist. Sie unterstützt derzeit noch kein allgemeines SystemVerilog, Power-Aware-Semantik, asynchrone Zeitplanung oder industrielle Netlisten in großem Maßstab. Das Paper unterscheidet zudem zwischen „Proof“ (exakte Erfüllung der kodierten Boole’schen Verpflichtung) und „Certification“ (was ein verifiziertes Frontend und eine Proof-Checker-Kette erfordert – beides als zukünftige Arbeiten markiert).

Zusammenfassend bietet TensorEQC einen Rahmen zur Kombination mehrerer exakter Verifizierungsmethoden zur Handhabung heterogener Logik. Es zeigt, dass – obwohl keine einzelne Engine universell optimal ist – ein strukturiertes Portfolio spezifische Schaltungsklassen effektiv verifizieren kann, während es gleichzeitig seine eigenen Grenzen klar identifiziert.