Btor2MLIR: A Format and Toolchain for Hardware Verification

Immagina di essere un detective che cerca di risolvere un mistero, ma gli indizi sono scritti in un codice segreto che solo pochi specialisti sanno leggere. Nel mondo dell'informatica, questo "codice segreto" è il linguaggio usato per descrivere come i chip dei computer (hardware) dovrebbero comportarsi. Gli ingegneri costruiscono questi chip per far funzionare tutto, dal tuo telefono ai satelliti nello spazio, ma se c'è anche un solo minuscolo errore nel design, l'intero sistema può crashare o comportarsi in modo strano. Per prevenire ciò, i ricercatori utilizzano i "metodi formali" — strumenti matematici che agiscono come super-correttori ortografici per dimostrare che un design sia perfetto prima che venga effettivamente costruito.

Per molto tempo, questi correttori ortografici parlavano lingue diverse. Alcuni parlavano "BTOR2", un formato popolare nelle competizioni hardware, mentre altri parlavano "LLVM-IR", un linguaggio usato dai compilatori software per controllare il codice. Era come avere un traduttore che sapeva tradurre solo dal francese all'inglese, e un altro che parlava solo dallo spagnolo all'inglese. Se volevi usare un traduttore francese per controllare un libro spagnolo, eri senza speranza. Dovevi costruire un intero nuovo traduttore da zero ogni volta. Questo articolo presenta un nuovo, magico traduttore chiamato BTOR2MLIR. Si posiziona nel mezzo, agendo come un ponte universale che permette ai design hardware di parlare con gli strumenti software senza dover reinventare la ruota ogni volta.

Il Problema: Troppi Dialetti, Pochi Ponti

Nel mondo della verifica hardware, il formato BTOR2 è diventato lo standard per descrivere i circuiti per competizioni come la Hardware Model Checking Competition (HWMCC). Pensa a BTOR2 come a un dialetto molto specifico ed efficiente per descrivere come un circuito digitale conta, somma numeri o controlla errori. Strumenti come BTORMC sono costruiti specificamente per leggere questo dialetto e controllare se il circuito è sicuro.

Tuttavia, il mondo della verifica software è enorme e potente. Strumenti come SEAHORN sono esperti nel controllare il codice software scritto nel linguaggio LLVM-IR. Questi strumenti sono incredibilmente maturi, perfezionati in decenni da enormi progetti come l'infrastruttura del compilatore LLVM. Possiedono funzionalità integrate per ottimizzare il codice, trovare bug ed eseguire simulazioni.

Il problema è che questi due mondi raramente si parlano. Per usare un potente strumento software per controllare un design hardware, i ricercatori dovevano scrivere traduttori personalizzati e una tantum. Era come cercare di inserire un perno quadrato in un foro rotondo ogni singola volta. Questi traduttori spesso dovevano reimplementare funzioni di base (come la gestione di numeri o cicli) che esistevano già negli strumenti software, portando a uno spreco di sforzi e a potenziali errori.

La Soluzione: L'Adattatore Universale (BTOR2MLIR)

Gli autori di questo articolo, Joseph Tafese, Isabel Garcia-Contreras e Arie Gurfinkel dell'Università del Waterloo, hanno deciso di costruire un ponte migliore. Hanno creato BTOR2MLIR, un nuovo formato e una catena di strumenti basata su MLIR (Multi-Level Intermediate Representation).

Per capire MLIR, immagina un enorme set di Lego modulari. Invece di costruire un intero nuovo castello da zero ogni volta che vuoi costruire un tipo diverso di casa, MLIR ti fornisce un set base di mattoncini (dialetti) che puoi incastrare tra loro. Puoi definire un nuovo "mattoncino hardware" che assomiglia e si comporta esattamente come BTOR2, ma che si incastra direttamente nella struttura "software" esistente.

Ecco come funziona il loro nuovo strumento:

1. Il Traduttore: Hanno costruito un "Dialetto BTOR" all'interno di MLIR. Questo è una traduzione diretta e lossless (senza perdita) del formato BTOR2. Se hai un file BTOR2, BTOR2MLIR può trasformarlo in questo dialetto MLIR istantaneamente.
2. Il Ponte: Poiché MLIR è progettato per essere estensibile, hanno creato una "passata di conversione" (conversion pass) che trasforma il loro Dialetto BTOR nel Dialetto LLVM standard. Questo è il passaggio magico. Prende la descrizione hardware e la trasforma in un formato che gli strumenti software come SEAHORN possono comprendere nativamente.
3. Il Risultato: L'output è LLVM-IR, un linguaggio che i motori di verifica software possono consumare e analizzare.

L'Esperimento: Funziona Davvero?

Il team non si è limitato a costruire il ponte; ci ha fatto passare sopra un camion per vedere se reggeva. Hanno preso una collezione di benchmark hardware reali dalla competizione HWMCC (specificamente i set 2020 e 2019) e li hanno fatti passare attraverso la loro nuova catena di strumenti.

Prima, hanno controllato la correttezza. Hanno preso un file BTOR2, lo hanno convertito nel loro formato MLIR e poi lo hanno convertito indietro in BTOR2. Hanno confrontato il file originale e quello sottoposto a round-trip. Il risultato? Erano identici. Le proprietà di sicurezza (le regole che il circuito deve seguire) sono state preservate perfettamente. Anche in casi complicati in cui gli strumenti originali andavano in timeout o esaurivano la memoria, le loro versioni round-tripped a volte hanno risolto il problema, suggerendo che la traduzione non ha introdotto errori.

Successivamente, hanno testato le prestazioni. Hanno collegato il loro strumento a SEAHORN, un famoso model checker per software, e BOOLECTOR, un solver veloce. Hanno confrontato questa nuova pipeline "ibrida" contro BTORMC, lo strumento gold-standard costruito specificamente per BTOR2.

I risultati sono stati sorprendenti e incoraggianti:

• Velocità: In molti casi, la pipeline ibrida (BTOR2MLIR + SEAHORN + BOOLECTOR) è stata competitiva con, e talvolta più veloce del, dedicato strumento BTORMC. Ad esempio, nella categoria di benchmark "19/mann", l'approccio ibrido ha risolto 44 istanze in circa 3.190 secondi, mentre BTORMC ha impiegato più tempo o è andato in timeout su più istanze.
• Flessibilità: Lo strumento ha gestito con successo operazioni complesse come la divisione e i vettori di bit (bit-vectors), dimostrando che i "mattoncini Lego" di MLIR possono gestire il lavoro pesante della logica hardware.
• Limitazioni: Gli autori sono stati onesti su ciò che il loro strumento non può ancora fare. Attualmente supporta bitvectors e array, ma non gestisce ancora i vincoli di "fairness" e "justice" (regole su come un sistema si comporta su un tempo infinito). Inoltre, sebbene funzioni bene, non ha completamente schiacciato gli strumenti dedicati all'hardware in ogni singola categoria; è stato un forte contendente, non un sostituto totale.

Perché Questo è Importante

L'articolo non sostiene di aver risolto tutta la verifica hardware. Inveve, suggerisce un nuovo modo di pensare. Utilizzando l'infrastruttura matura e robusta del compilatore LLVM (che alimenta strumenti per tutto, dai videogiochi ai browser web), i ricercatori hardware possono smettere di reinventare la ruota.

Gli autori dimostrano che è possibile prendere un design hardware, tradurlo in un linguaggio universale e poi usare potenti strumenti software esistenti per controllarlo. Questo apre la porta alla prototipazione rapida. Se un ricercatore vuole provare una nuova tecnica di verifica, non ha bisogno di costruire un intero nuovo motore; deve solo collegare la sua idea al framework MLIR.

In futuro, il team prevede di collegare questo ponte ad ancora più strumenti, come KLEE (un motore di esecuzione simbolica) e LIBFUZZER (uno strumento di fuzzing), che sono attualmente usati per il software ma potrebbero rivoluzionare il modo in cui troviamo i bug nell'hardware. Prevedono anche di generare altri formati come AIGER e SMT-LIB.

In definitiva, BTOR2MLIR è una prova di concetto che le barriere tra la verifica hardware e quella software stanno cadendo. Suggerisce che, parlando un linguaggio comune, possiamo rendere il nostro mondo digitale più sicuro, veloce e facile da costruire.