Formal that "Floats" High: Formal Verification of Floating Point Arithmetic

Questo articolo presenta una metodologia scalabile per la verifica formale dell'aritmetica in virgola mobile a livello RTL, che combina un approccio modulare di tipo "divide et impera", l'iniezione di fault e la generazione assistita da intelligenza artificiale per superare le limitazioni dei modelli ad alto livello e migliorare l'efficienza della copertura.

L'essenziale

Immagina di dover costruire un orologio di precisione microscopico, fatto di miliardi di ingranaggi di silicio. Se anche un solo ingranaggio gira di un milionesimo di secondo in più o in meno, l'intero orologio potrebbe smettere di funzionare o, peggio, dare un'ora sbagliata in un momento critico.

Questo è il mondo dei processori moderni e, in particolare, di come calcolano i numeri con la virgola (i numeri "floating-point"), usati per tutto, dai videogiochi alle missioni spaziali.

Ecco di cosa parla questo articolo, spiegato come se stessimo chiacchierando al bar:

1. Il Problema: "Tradurre" è pericoloso

Fino a poco tempo fa, per controllare se questi circuiti funzionavano bene, gli ingegneri facevano una cosa un po' rischiosa: prendevano il progetto del chip (scritto in un linguaggio chiamato RTL, che è come il piano di costruzione dettagliato) e lo "traducevano" in un linguaggio di programmazione più semplice (come il C), per poi confrontarlo con un modello teorico.

È come se avessi un'architettura di un grattacielo in disegni tecnici complessi, e per controllarla la dessi a un traduttore che la riscrive in una poesia. Poi confronti la poesia con il progetto originale.

• Il rischio: Il traduttore potrebbe aver sbagliato una parola, o la poesia potrebbe non catturare la forza di un ingranaggio che si rompe. C'è un "vuoto" tra la poesia e il mattone reale.

2. La Soluzione Proposta: Il "Gemello Digitale" Perfetto

Gli autori di questo articolo (che lavorano per Infineon, un gigante dei chip) dicono: "Basta traduzioni!".
Hanno creato un metodo per confrontare direttamente il progetto reale (RTL) con un modello di riferimento perfetto (anch'esso in RTL, ma scritto in modo semplice e matematicamente corretto, come un "gemello digitale" ideale).

È come se avessi due orologi identici:

1. L'Orologio Reale (quello che stai costruendo).
2. L'Orologio Maestro (quello che sai per certo che funziona alla perfezione).

Invece di tradurre l'orologio reale in parole, lo metti a confronto diretto con il Maestro, ingranaggio per ingranaggio, istante per istante. Se anche un solo dente di un ingranaggio è diverso, il sistema lo vede subito.

3. La Strategia: "Dividi e Comanda"

Controllare un intero chip complesso tutto in una volta è come cercare di trovare un ago in un pagliaio mentre il pagliaio brucia. È troppo difficile.
Il loro metodo usa una strategia di "Dividi e Comanda":

• Scompongono l'operazione matematica (es. sommare due numeri con la virgola) in piccoli passi semplici: prima allineano i numeri, poi li sommano, poi arrotondano il risultato.
• Controllano ogni piccolo passo separatamente. Se il primo passo è sbagliato, lo sistemano prima di passare al secondo. È come controllare una ricetta: prima assaggi se hai messo il sale, poi se la pasta è cotta, non tutto insieme alla fine.

4. L'Intelligenza Artificiale: Il "Tirocinante Geniale ma Distratto"

Qui entra in gioco la parte più moderna e creativa del paper. Hanno usato l'Intelligenza Artificiale (specificamente dei modelli linguistici come GPT) per scrivere le regole di controllo (le "asserzioni").

Immagina di avere un tirocinante geniale (l'AI) che conosce la teoria perfetta ma non ha mai visto un vero orologio in mano.

• Senza supervisione: Il tirocinante scrive 15 regole per controllare l'orologio. Molte sono ridondanti (ripetono la stessa cosa), altre sono confuse. È come se ti desse 100 mappe, ma 90 portano in posti sbagliati.
• Con supervisione (HITL - Human in the Loop): Un ingegnere esperto (l'umano) guarda il lavoro del tirocinante e dice: "Ehi, questa regola è inutile, e quest'altra è sbagliata perché non hai considerato che l'orologio può fermarsi".
• Risultato: Dopo un po' di correzioni, il tirocinante AI produce solo 3 regole perfette che coprono tutto il lavoro.

5. I Risultati: Cosa hanno scoperto?

• Confronto diretto: Controllare il chip direttamente contro il "gemello digitale" è molto più veloce e preciso che usare traduzioni.
• L'AI funziona, ma... L'AI da sola fa confusione se non ha un "modello di riferimento" (il gemello perfetto) davanti agli occhi. Se deve controllare il chip da sola, senza sapere come dovrebbe funzionare, si perde.
• Il mix vincente: Quando l'AI lavora con un modello di riferimento e viene guidata da un umano, diventa potentissima. Trova errori che gli umani potrebbero saltare e lo fa velocemente.

In Sintesi

Questo articolo ci dice che per costruire i chip del futuro (che devono essere perfetti al 100%), non dobbiamo più affidarci a traduzioni approssimative. Dobbiamo confrontare direttamente il progetto con la perfezione matematica. E, cosa ancora più bella, possiamo usare l'Intelligenza Artificiale come un assistente super-veloce, purché un esperto umano gli tenga la mano e gli dica: "Sì, questa è la strada giusta".

È come avere un navigatore satellitare (l'AI) che ti dice la strada, ma hai bisogno di un pilota esperto (l'ingegnere umano) per assicurarsi che il GPS non ti stia portando nel deserto. Insieme, arrivano a destinazione in modo sicuro e veloce.

Sommario tecnico

Ecco una sintesi tecnica dettagliata del documento in italiano, strutturata secondo le sezioni richieste.

Titolo: Verifica Formale dell'Aritmetica in Virgola Mobile: Un Approccio Scalabile RTL-to-RTL con Integrazione di IA Agente

1. Il Problema

La verifica formale dell'aritmetica in virgola mobile (Floating-Point Arithmetic) rappresenta una delle sfide più complesse nella progettazione hardware moderna. Le difficoltà principali derivano da:

• Comportamento non lineare: La natura matematica delle operazioni in virgola mobile (allineamento degli esponenti, normalizzazione, arrotondamento) crea spazi di stato complessi.
• Accoppiamento stretto: L'interazione tra la logica di controllo (gestione delle eccezioni, overflow, underflow) e il percorso dati aritmetico rende difficile l'esplorazione esaustiva.
• Limiti degli approcci esistenti: Le metodologie attuali si basano spesso su modelli di riferimento ad alto livello (es. C/C++) per il controllo di equivalenza rispetto al livello RTL (Register Transfer Level). Questo introduce:
  • Divari di astrazione: Discrepanze semantiche tra l'esecuzione software e l'hardware.
  • Overhead di traduzione: Necessità di convertire il RTL in C o viceversa, aumentando il rischio di errori.
  • Scalabilità ridotta: Difficoltà nell'applicare questi flussi a progetti RTL complessi e specifici per il datapath.

2. Metodologia Proposta

Gli autori presentano una metodologia di verifica formale che elimina la dipendenza da modelli software ad alto livello, adottando un approccio diretto RTL-to-RTL.

• Verifica RTL-to-RTL: Confronto diretto tra l'implementazione RTL (Design Under Verification - DUV) e un modello di riferimento "Golden" anch'esso in RTL (SystemVerilog), garantendo una precisione bit-per-bit conforme allo standard IEEE-754.
• Strategia "Divide and Conquer" (Decomposizione Gerarchica):
  • Il design (un addizionale in virgola mobile) viene scomposto in fasi modulari: Mantissa Alignment Stage e Add-Round Stage.
  • Viene utilizzato un approccio basato su teoremi e lemmi: un teorema principale di equivalenza è dimostrato attraverso lemmi intermedi che verificano la correttezza di ogni fase.
  • Raffinamento guidato da CEX (Counterexample): Se il verificatore formale trova un errore, il CEX viene utilizzato per isolare il difetto, correggere l'implementazione o affinare le proprietà, iterando fino alla prova completa.
• Generazione di Proprietà tramite IA Agente:
  • È stato implementato un sistema multi-agente (MAS) che utilizza Large Language Models (LLM) come GPT-5 e Llama3.3.
  • Flusso di lavoro: Un Lead Agent pianifica la verifica, un Property Generation Agent traduce le specifiche in SystemVerilog Assertions (SVA), un Critic Agent valuta la correttezza logica e un Error Correction Agent risolve i problemi.
  • Human-in-the-Loop (HITL): Gli esperti umani intervengono per chiarire le ambiguità e guidare il raffinamento delle proprietà, specialmente quando l'IA non converge autonomamente.

3. Contributi Chiave

1. Verifica Diretta RTL-to-RTL: Eliminazione dei modelli C di riferimento, permettendo una verifica esaustiva e priva di ambiguità semantiche a livello di implementazione hardware.
2. Strategia di Decomposizione Modulare: Scomposizione del problema di verifica in fasi gestibili (allineamento mantissa, addizione/arrotondamento) supportata da asserzioni di aiuto, che migliora la convergenza della prova.
3. Rilevamento e Risoluzione di Bug: Identificazione e correzione di difetti reali nell'implementazione (es. selezione errata degli operandi, logica di inversione difettosa) tramite l'analisi dei CEX.
4. Iniezione di Guasti (Fault Injection): Validazione della robustezza del processo di verifica introducendo guasti controllati nel datapath per verificare la capacità delle proprietà formali di rilevarli.
5. Analisi di Copertura con IA: Confronto empirico tra proprietà scritte manualmente e quelle generate da LLM, valutando l'efficacia dell'approccio ibrido (IA + HITL) in scenari con e senza modello di riferimento.

4. Risultati

Gli esperimenti sono stati condotti su un addizionale in virgola mobile a singola precisione utilizzando la piattaforma Cadence Jasper Formal.

• Rilevamento di Bug: La metodologia ha identificato e corretto errori critici nell'implementazione, come una selezione errata degli operandi quando gli esponenti erano uguali e una logica di inversione errata durante la sottrazione.
• Robustezza: L'iniezione di 8 guasti diversi (4 per fase) è stata rilevata con successo da tutte le proprietà formali, dimostrando l'efficacia nel catturare errori di precisione.
• Efficienza della Copertura (RTL-to-RTL):
  • Le asserzioni scritte manualmente hanno raggiunto una copertura formale del 98,42% con sole 2 proprietà e un tempo di prova di 0,073s.
  • Le proprietà generate da LLM (senza HITL) richiedevano più asserzioni (7-15) e tempi di prova superiori, spesso con ridondanza.
  • Con il raffinamento HITL, i LLM (in particolare GPT-5) hanno raggiunto una copertura simile a quella manuale (98,42%) con un numero ridotto di asserzioni (3-6) e tempi di prova competitivi (1,318s per GPT-5).
• Verifica Standalone (Senza Modello di Riferimento):
  • Senza un modello Golden, la copertura è crollata significativamente (es. 62,13% per Llama3.3 senza HITL) a causa della difficoltà degli LLM nel vincolare correttamente il comportamento micro-architettonico.
  • Anche con HITL, la copertura è migliorata (fino al 92,30% per GPT-5), ma ha richiesto un numero molto maggiore di asserzioni (21) e un intervento umano sostanziale per correggere assunzioni errate.

5. Significato e Impatto

Questo lavoro dimostra che la verifica formale diretta RTL-to-RTL è superiore agli approcci basati su modelli C per i datapath aritmetici complessi, offrendo maggiore precisione e scalabilità.
L'integrazione di IA Agente con supervisione umana (HITL) si rivela una strategia promettente:

• Riduce lo sforzo manuale nella scrittura di proprietà formali.
• Mantiene un'alta efficienza di copertura quando supportata da un modello di riferimento Golden.
• Evidenzia che, sebbene gli LLM siano potenti, la loro applicazione in scenari "standalone" (senza riferimento) richiede ancora un significativo intervento umano per comprendere le sottigliezze micro-architettoniche.

In conclusione, la metodologia proposta stabilisce una base solida per la verifica scalabile assistita da IA, suggerendo che il futuro della verifica formale risiede in un ciclo iterativo dove l'IA genera ipotesi e l'esperto umano fornisce il contesto architetturale necessario per la validazione.