Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement

Nel mondo invisibile dei microchip, dove miliardi di transistor si accendono e si spengono per alimentare tutto, dagli smartphone alle navicelle spaziali, un singolo errore nascosto può causare il fallimento catastrofico di un sistema. Gli ingegneri progettano questi chip utilizzando un linguaggio chiamato Register Transfer Level, o RTL, che descrive come i dati si muovono tra gli elementi di memoria nel tempo. Per garantire che questi progetti funzionino correttamente prima di essere costruiti, gli esperti di verifica scrivono delle "assertion" (asserzioni). Pensate a un'asserzione come a una regola rigorosa scritta all'interno del design stesso, un'affermazione che dice: "Se accade questo, allora deve seguire quello". Se il chip viola mai questa regola, il sistema lancia un allarme, rivelando un bug che altrimenti potrebbe passare inosservato. Per decenni, scrivere queste regole è stato un compito lento, manuale e soggetto a errori, che richiedeva agli ingegneri di indovinare quali comportamenti potessero andare storti e scrivere controlli specifici per essi. Sebbene i computer abbiano aiutato estraendo schemi dalle simulazioni di design esistenti, questi metodi automatizzati spesso perdono gli scenari più pericolosi semplicemente perché i test casuali su cui si basano non inciampano mai in essi.

Un team di ricercatori della The Hong Kong University of Science and Technology (Guangzhou) ha sviluppato un nuovo approccio per risolvere questo problema, chiamando il loro sistema NeuroAssertion. Invece di affidarsi al caso, il loro metodo cerca attivamente i comportamenti più difficili da raggiungere in un design di un chip e poi utilizza una combinazione di intelligenza artificiale e logica formale per scrivere le necessarie regole di sicurezza. Il processo inizia trasformando il design per renderlo più facile da analizzare per vedere quali parti vengono testate. I ricercatori inseriscono speciali marcatori nel codice che tracciano se specifiche condizioni difficili da attivare si siano mai verificate. Utilizzano poi un potente motore matematico, noto come model checker, per forzare il design a eseguire quelle condizioni rare. Ciò genera un insieme di casi di test altamente specifici che espongono comportamenti che le simulazioni casuali probabilmente mancherebbero per sempre. Queste nuove e diverse tracce forniscono una base molto più ricca per la fase successiva.

Una volta che il sistema ha ottenuto questi comportamenti difficili da trovare, passa alla fase di generazione. Utilizza una tecnica chiamata sintesi guidata dalla sintassi (syntax-guided synthesis) per creare regole di sicurezza iniziali basate sui dati osservati. Tuttavia, i ricercatori hanno riconosciuto che questo primo passaggio è raramente perfetto. Per risolvere il problema, hanno introdotto un ciclo di raffinamento che agisce come un editor rigoroso. Il sistema misura quanto bene l'attuale set di regole possa rilevare i cambiamenti nel design iniettando piccoli errori deliberati, noti come mutanti, nel codice. Se le regole non riescono a rilevare un mutante, il sistema sa esattamente quale comportamento rimane non controllato. Interroga quindi un grande modello linguistico affinché proponga una nuova regola progettata specificamente per colmare quel vuoto. Se la regola proposta è logicamente errata, un secondo modello linguistico non la scarta; invece, analizza l'errore e costruisce un insieme specializzato di istruzioni, o grammatica, per guidare un risolutore simbolico nel riparare la regola. Si crea così un ciclo in cui il sistema propone, controlla e corregge le asserzioni finché non sono sia numerose che robuste.

I risultati di questo approccio sono stati testati su sette diversi design di chip, che vanno da piccoli circuiti di arbitraggio a complessi core di processori. Il nuovo framework ha costantemente superato il precedente stato dell'arte, noto come SMART, che si basa su un singolo passaggio di estrazione senza questo raffinamento attivo. In questi esperimenti, NeuroAssertion ha generato circa il doppio delle asserzioni rispetto al metodo precedente. Più importante ancora, la qualità di queste regole era significativamente più alta. Misurata in base alla loro capacità di rilevare errori iniettati, il nuovo sistema ha raggiunto circa il doppio della copertura rispetto all'approccio tradizionale. Su alcuni benchmark specifici, il miglioramento è stato ancora più drammatico; ad esempio, su un componente di un processore, la copertura delle mutazioni è passata da circa il sei percento a oltre il trentadue percento. I ricercatori hanno anche confrontato il loro sistema con un approccio diretto in cui un grande modello linguistico veniva interrogato per scrivere regole senza alcun passaggio di controllo formale o raffinamento. Quel metodo diretto ha prodotto molte meno regole ed è fallito nel rilevare la maggior parte dei potenziali errori, dimostrando che la pura generazione linguistica da sola è insufficiente per questo compito ad alto rischio.

Trattando la generazione di asserzioni come un ciclo continuo di esplorazione e raffinamento piuttosto che come un evento unico, i ricercatori hanno dimostrato che è possibile automatizzare la creazione di regole di sicurezza di alta qualità per l'hardware complesso. Il sistema non si limita a indovinare; cerca attivamente i punti ciechi in un design e utilizza una partnership tra reti neurali e logica formale per colmarli. Questo lavoro suggerisce che il futuro della verifica dell'hardware risiede nell'unire il riconoscimento di schemi dell'intelligenza artificiale con la certezza rigorosa della prova matematica, garantendo che i chip che alimentano il nostro mondo siano affidabili quanto gli ingegneri che li progettano.