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

Sintesi Tecnica: TensorEQC – Verifica di Equivalenza Sensibile alla Struttura

Problematica
La verifica di equivalenza (EC) è altamente sensibile alla rappresentazione di un circuito. Diverse strutture di circuiti — come le reti ricche di XOR, le catene di carry, i moltiplicatori in campi finiti e i moltiplicatori interi — esibiscono proprietà strutturali distinte che favoriscono diversi approcci di verifica. Nessun metodo singolo (ad esempio, l'algebra booleana, i diagrammi decisionali o le reti tensoriali) domina universalmente tutti i tipi di circuiti. Inoltre, la verifica di circuiti sequenziali richiede di distinguere tra la dipendenza dallo stato iniziale osservabile e l'incertezza che si risolve entro un limite di osservazione specifico, in particolare riguardo agli stati di reset.

Metodologia
Il documento presenta TensorEQC, un workflow di ricerca eseguibile progettato come un portfolio multi-algoritmico piuttosto che come un singolo solver monolitico. La sua filosofia centrale è che un motore debba scaricare un obbligo di verifica solo se può farlo secondo la propria semantica esatta; in caso contrario, l'obbligo viene passato a un altro motore.

Il workflow consiste in tre componenti primarie:

1. Portfolio Combinatorio: Una pipeline sequenziale di motori di verifica che elabora gli output finché non vengono scaricati o finché non viene raggiunto un limite di risorse. La pipeline include:
   • Hashing Strutturale: Stabilisce l'identità dei DAG di espressione sotto i primitivi supportati (AND, OR, XOR, ecc.) con normalizzazione commutativa.
   • Simulazione: Utilizza la simulazione pacchettizzata con pattern casuali, tutti-zero e tutti-uno per trovare testimoni negativi (controesempi).
   • Forme Normali Algebriche (ANF): Rappresenta le funzioni booleane come polinomi multilineari su GF(2). Utilizza un lemma specifico per generare testimoni negativi esatti da polinomi non nulli.
   • Eliminazione Tensoriale Relazionale: Rappresenta le porte come tensori indicatori booleani. Esegue l'eliminazione delle variabili tramite disgiunzione sul semianello booleano (per preservare l'esistenza di assegnazioni soddisfacenti) piuttosto che la sommatoria su GF(2) (che calcola la parità).
   • ROBDD & Fallback Esaustivo: Utilizza Ordered Binary Decision Diagrams con limiti di nodo (node caps) ed enumerazione esaustiva a supporto ridotto come fallback finali.
2. Analisi Tensor Train (TT): Un modulo complementare che costruisce rappresentazioni TT esatte dalle tavole della verità per misurare il rango algebrico e testare la presenza di funzioni nulle. Distingue tra i ranghi su GF(2) e sui numeri reali, notando che i ranghi su GF(2) possono essere significativamente più piccoli.
3. Analisi del Reset: Un modulo sincrono che utilizza l'auto-composizione a stato esplicito per controllare la dipendenza dallo stato iniziale. Distingue tra i casi in cui la dipendenza dal reset è osservabile immediatamente e i casi in cui scompare dopo un numero specifico di cicli di "flushing".

Contributi Chiave

• Integrazione di Motori Esatti: Il lavoro dimostra un'integrazione pratica di hashing strutturale, algebra GF(2), reti tensoriali relazionali e ROBDD, mantenendo distinti i contratti di prova per ciascuno.
• Strategia Sensibile alla Struttura: Fornisce prove empiriche che l'efficienza della verifica dipende fortemente dalla struttura del circuito e dall'ordinamento delle variabili. Ad esempio, gli operandi di un addizionatore intercalati producono bassi ranghi tensoriali (≤3), mentre gli operandi divisi risultano in ranghi elevati (129), rendendo questi ultimi meno adatti agli approcci basati su tensori.
• Diagnostica dello Stato di Reset: Offre un metodo per distinguere esplicitamente tra vera dipendenza dallo stato iniziale e incertezza transitoria nei design sincroni.
• Validazione Riproducibile: Il documento include un nuovo supplemento autocontenuto che valida la costruzione di tensor train esatti su GF(2), le misurazioni del rango e i test di funzione nulla su cinque funzioni a 16 ingressi, confermando la distinzione tra cancellazione della parità e funzioni effettivamente nulle.

Risultati Sperimentali
Lo studio riporta due distinti set di evidenze:

1. Campagna del Portfolio Storico (v1.0.0): Questo dataset include 89 esecuzioni riguardanti ripple adder a 2.048 bit, moltiplicatori a base polinomiale a 128 bit e reti affini.
   • Successi: Il flusso completo ha verificato con successo ripple adder a 2.048 bit (2,87s) e moltiplicatori GF a 128 bit (0,80s), superando gli approcci basati solo su BDD in casi specifici (ad esempio, adder a 2.048 bit dove i BDD non riuscivano a risolvere).
   • Limitazioni: L'approccio ha raggiunto i limiti di risorse (limiti di nodi, limiti di ampiezza) su ripple adder a 1.024 bit e reti affini a 1.024 ingressi. I risultati della moltiplicazione intera sono stati limitati a 10 bit a causa della crescita dell'ANF e dei limiti di ambito tensoriale.
   • Osservazione: Il flusso completo a volte incorre in un overhead rispetto alla selezione diretta del motore ottimale, evidenziando il compromesso tra automazione ed efficienza.
2. Nuovo Supplemento Riproducibile: Un esperimento focalizzato su cinque funzioni a 16 ingressi (inclusi parità e moltiplicazione GF) ha confermato che la costruzione di tensor train esatti e l'analisi del rango sono fattibili per funzioni piccole. Ha validato che una somma scalare GF(2) pari a zero non implica una funzione nulla (cancellazione della parità), una distinzione correttamente gestita dal test di zero del TT.

Significatività e Rivendicazioni
Il documento inquadra esplicitamente il proprio contributo come una valutazione tecnica delimitata piuttosto che una soluzione universale.

• Nessuna Superiorità Universale: I risultati non supportano la tesi che le reti tensoriali siano superiori a tutti gli altri metodi. Al contrario, supportano una "strategia sensibile alla rappresentazione" dove diversi motori vengono selezionati in base al dominio matematico (ad esempio, l'algebra GF per funzioni a campo finito a basso grado, l'eliminazione relazionale per le catene di carry).
• Integrazione anziché Sostituzione: Il risultato centrale è la riuscita integrazione di algebra esatta, eliminazione relazionale, diagrammi decisionali e ragionamento temporale, mantenendo distinti i relativi contratti di prova.
• Confini Espliciti: L'autore sottolinea che l'implementazione attuale è limitata a primitivi booleani combinatori e piccole macchine sincrone. Non supporta ancora SystemVerilog generico, semantica aware del consumo energetico, timing asincrono o netlist di scala industriale. Il documento distingue tra "prova" (soddisfacimento esatto dell'obbligo booleano codificato) e "certificazione" (che richiede una catena di frontend e controllore di prova verificata, entrambe indicate come lavori futuri).

In sintesi, TensorEQC fornisce un framework per combinare molteplici metodi di verifica esatta per gestire la logica eterogenea, dimostrando che, sebbene nessun motore sia universalmente ottimale, un portfolio strutturato può verificare efficacemente specifiche classi di circuiti identificando chiaramente i propri limiti.