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 Samenvatting: TensorEQC – Structuurbewuste Equivalentiecontrole

Probleemstelling
Equivalentiecontrole (EC) is zeer gevoelig voor de representatie van een circuit. Verschillende circuitstructuren—zoals XOR-rijke netwerken, carry-ketens, eindveld-multiplicatoren en integer-multiplicatoren—vertonen onderscheidende structurele eigenschappen die verschillende verificatiebenaderingen bevoordelen. Geen enkele methode (bijv. Booleaanse algebra, beslissingsdiagrammen of tensornetwerken) domineert universeel alle circuittypen. Bovendien vereist het verifiëren van sequentiële circuits het onderscheid tussen observeerbare initiële-toestandsafhankelijkheid en onzekerheid die binnen een specifieke observatiegrens wordt opgelost, met name met betrekking tot reset-toestanden.

Methodologie
Het paper introduceert TensorEQC, een uitvoerbare research-workflow die is ontworpen als een multi-algoritmisch portfolio in plaats van een enkele monolithische solver. De kernfilosofie is dat een engine alleen een verificatieverplichting mag vervullen als dit kan volgens de eigen exacte semantiek; anders wordt de verplichting doorgegeven aan een andere engine.

De workflow bestaat uit drie primaire componenten:

1. Combinatorieel Portfolio: Een sequentiële pijplijn van verificatie-engines die outputs verwerkt totdat ze zijn vervuld of totdat een resourcelimiet wordt bereikt. De pijplijn omvat:
   • Structurele Hashing: Stelt de identiteit van expressie-DAG's vast onder ondersteunde primitieven (AND, OR, XOR, etc.) met commutatieve normalisatie.
   • Simulatie: Gebruikt gepakte simulatie met willekeurige, alle-nul en alle-één patronen om negatieve getuigen (tegenvoorbeelden) te vinden.
   • Algebraïsche Normale Vormen (ANF): Representeert Booleaanse functies als multilineaire polynomen over GF(2). Het maakt gebruik van een specifieke lemma om exacte negatieve getuigen te genereren uit niet-nullo de polynomen.
   • Relationele Tensor Eliminatie: Representeert poorten als Booleaanse indicator-tensoren. Het voert variabele-eliminatie uit via disjunctie over de Booleaanse semiring (om de existentie van bevredigende toewijzingen te behouden) in plaats van GF(2)-sommatie (wat pariteit berekent).
   • ROBDD & Exhaustieve Fallback: Gebruikt Ordered Binary Decision Diagrams met node-caps en kleine-support exhaustieve enumeratie als laatste fallback-opties.
2. Tensor Train (TT) Analytics: Een begeleidend module die exacte TT-representaties construeert uit waarheidstafels om de algebraïsche rang te meten en te testen op nul-functies. Het maakt onderscheid tussen rangen over GF(2) en reële getallen, waarbij wordt opgemerkt dat GF(2)-rangen aanzienlijk kleiner kunnen zijn.
3. Reset-Analyse: Een synchrone module die gebruikmaakt van expliciete-toestand zelfcompositie om te controleren op initiële-toestandsafhankelijkheid. Het maakt onderscheid tussen gevallen waarin reset-afhankelijkheid onmiddellijk observeerbaar is en gevallen waarin deze verdwijnt na een specifiek aantal "flushing"-cycli.

Belangrijkste Bijdragen

• Integratie van Exacte Engines: Het werk demonstreert een praktische integratie van structurele hashing, GF(2)-algebra, relationele tensornetwerken en ROBDD's, waarbij de afzonderlijke bewijscontracten worden gehandhaafd.
• Structuurbewuste Strategie: Het levert empirisch bewijs dat de efficiëntie van verificatie sterk afhankelijk is van de circuitstructuur en de volgorde van variabelen. Zo leveren geïnterleavde adder-operanden een lage tensorrang op (≤3), terwijl gesplitste operanden een hoge rang resulteren (129), wat de laatste minder geschikt maakt voor tensor-gebaseerde benaderingen.
• Reset-Toestand Diagnostiek: Het biedt een methode om expliciet onderscheid te maken tussen ware initiële-toestandsafhankelijkheid en transiënte onzekerheid in synchrone ontwerpen.
• Reproduceerbare Validatie: Het paper bevat een nieuw, zelfstandig supplement dat de exacte GF(2) tensor train-constructie, rangmetingen en nul-functie tests op vijf 16-input functies valideert, waarmee het onderscheid tussen pariteitsannulering en werkelijke nul-functies wordt bevestigd.

Experimentele Resultaten
De studie rapporteert over twee verschillende sets bewijslast:

1. Historische Portfolio Campagne (v1.0.0): Deze dataset bevat 89 casus-runs met 2.048-bit ripple adders, 128-bit polynoom-basis multiplicatoren en affine netwerken.
   • Successen: De volledige flow verifieerde succesvol 2.048-bit ripple adders (2,87s) en 128-bit GF multiplicatoren (0,80s), waarmee het in specifieize gevallen (bijv. 2.048-bit adders waar BDD's faalden) BDD-alleen benaderingen overtrof.
   • Beperkingen: De aanpak liep tegen resourcelimieten aan (node caps, width caps) bij 1.024-bit ripple adders en 1.024-input affine netwerken. De resultaten voor integer-multiplicatie waren beperkt tot 10 bits vanwege de groei van ANF en de tensor scope caps.
   • Observatie: De volledige flow bracht soms overhead met zich mee vergeleken met het direct selecteren van de optimale engine, wat de afruil tussen automatisering en efficiëntie benadrukt.
2. Nieuw Reproduceerbaar Supplement: Een gerichte experiment op vijf 16-input functies (inclusief pariteit en GF multiplicatie) bevestigde dat exacte tensor train constructie en ranganalyse haalbaar zijn voor kleine functies. Het valideerde dat een scalaire GF(2) som van nul niet impliceert dat het een nul-functie is (pariteitsannulering), een onderscheid dat correct wordt afgehandeld door de TT nul-test.

Betekenis en Claims
Het paper kadert zijn bijdrage expliciet als een gekwantificeerde technische beoordeling in plaats van een universele oplossing.

• Geen Universele Superieuriteit: De resultaten ondersteunen de claim niet dat tensornetwerken superieur zijn aan alle andere methoden. In plaats daarvan ondersteunen ze een "representatie-gevoelige strategie" waarbij verschillende engines worden geselecteerd op basis van het wiskundige domein (bijv. GF algebra voor functies met een lage graad in eindvelden, relationele eliminatie voor carry-ketens).
• Integratie boven Vervanging: Het centrale resultaat is de succesvolle integratie van exacte algebra, relationele eliminatie, beslissingsdiagrammen en temporele redenering, terwijl de afzonderlijke bewijscontracten intact blijven.
• Expliciete Grenzen: De auteur benadrukt dat de huidige implementatie beperkt is tot binaire combinatorische primitieven en kleine synchrone machines. Het ondersteunt nog geen algemene SystemVerilog, power-aware semantiek, asynchrone timing of industriële netlijsten. Het paper maakt onderscheid tussen "bewijs" (exacte voldoening van de gecodeerde Booleaanse verplichting) en "certificering" (wat een geverifieerde frontend en een bewijscontroleur-keten vereist, beide vermeld als toekomstig werk).

Samenvattend biedt TensorEQC een raamwerk voor het combineren van meerdere exacte verificatiemethoden om heterogene logica aan te pakken, waarbij wordt aangetoond dat hoewel geen enkele engine universeel optimaal is, een gestructureerd portfolio specifieke circuitklassen effectief kan verifiëren terwijl het zijn eigen beperkingen duidelijk identificeert.