Riepilogo Tecnico: SpecAlign – Un Framework di Allineamento Semantico per la Generazione di Asserzioni SystemVerilog

1. Enunciato del Problema

La crescente complessità dei progetti hardware moderni ha spinto l'adozione di Modelli Linguistici di grandi dimensioni (LLM) per la generazione di asserzioni SystemVerilog (SVA) a supporto della verifica basata su asserzioni (ABV). Tuttavia, gli approcci esistenti basati su LLM si concentrano principalmente sulla validità sintattica e sui risultati della verifica formale (FV) (ad esempio, se un'asserzione è dimostrata o produce un controesempio su un determinato RTL). Queste metriche non affrontano l'allineamento semantico: se l'asserzione generata riflette accuratamente l'intento comportamentale descritto nella specifica in linguaggio naturale.

Gli LLM possono produrre asserzioni che sono sintatticamente corrette e formalmente dimostrabili su una specifica implementazione RTL, ma che sono semanticamente inefficaci o allucinate. Ad esempio, un'asserzione potrebbe campionare un clock sullo stesso bordo che attiva la proprietà, rendendola vuota (vacuous) nonostante superi la FV. In assenza di un modello RTL "golden" per il confronto, l'ispezione manuale di tali asserzioni è dispendiosa in termini di tempo e riduce la fiducia. Inoltre, i motori FV affrontano problemi di scalabilità (esplosione dello spazio degli stati) quando valutano grandi insiemi di asserzioni generate per progetti complessi. Vi è un bisogno critico di un framework che valuti la coerenza semantica rispetto alla specifica stessa, indipendentemente dai dettagli di implementazione RTL.

2. Metodologia: Il Framework SpecAlign

SpecAlign è un framework centrato sulla specifica progettato per valutare e raffinare iterativamente le SVA generate da LLM senza fare affidamento su un RTL golden. Opera attraverso due loop iterativi principali: un Loop di Allineamento delle Proprietà e un Loop di Allineamento delle SVA. Entrambi i loop utilizzano tre fasi fondamentali: Controllo di Allineamento, Analisi delle Incoerenze ed Estrazione di Evidenze.

A. Panoramica Architetturale

Il framework normalizza il confronto tra diverse rappresentazioni dell'intento di progetto. Mentre l'input consiste in proprietà in linguaggio naturale ($P$) e SVA generate ($A$), il framework converte ogni SVA in un Riassunto in Linguaggio Naturale ($N$) tramite un processo di estrazione specifico. Questa normalizzazione permette di valutare sia le proprietà che le asserzioni allo stesso livello semantico rispetto alla specifica di progetto ($S$).

B. Componenti Principali

1. Controllo di Allineamento:

   • Classificazione: Il framework classifica le descrizioni in linguaggio naturale ($X_i$) in tre categorie in base alla loro relazione con la specifica:
     • Implica (Entails): Tutti gli elementi sono supportati dalla specifica.
     • Contraddice (Contradicts): Almeno un elemento contraddice la specifica.
     • Sconosciuto (Unknown): Gli elementi non sono né supportati né contraddetti (spesso a causa di assunzioni specifiche dell'implementazione non presenti nella specifica).
   • Votazione per Coerenza Interna: Per migliorare l'affidabilità, il sistema adotta una strategia di prompting Chain-of-Thought (CoT). Genera $k$ percorsi di ragionamento per un dato input e aggrega i sottoverdetti utilizzando la votazione a maggioranza. In caso di parità, viene applicata una priorità conservativa: Contraddice > Sconosciuto > Implica.
   • Selezione del Riferimento: Il Loop delle Proprietà utilizza la specifica di progetto ($S$) come riferimento. Il Loop delle SVA utilizza una "Banca di Proprietà Allineate" (se disponibile) per ridurre il rumore derivante da documenti di specifica dispersi; in caso contrario, fa ricorso a $S$.

2. Analisi delle Incoerenze e Raffinamento:

   • Quando il verdetto è Contraddice, il sistema esegue un'Analisi delle Incoerenze. Identifica gli elementi specifici in conflitto nella descrizione, fa riferimento al comportamento corretto nella specifica e genera feedback strutturati e azionabili ($F_i$).
   • Questo feedback guida l'LLM a rigenerare la proprietà o l'asserzione ($P'_i$ o $A'_i$), definendo esplicitamente le condizioni di attivazione ed evitando l'introduzione di nuovi segnali o comportamenti non presenti nella specifica.
   • L'output raffinato viene riesaminato nel loop di allineamento fino al raggiungimento di un numero fisso di iterazioni o all'allineamento dell'output.

3. Estrazione di Evidenze:

   • Per i casi Implica, il sistema estrae evidenze di supporto (citazioni e posizioni) dalla specifica per facilitare la revisione umana e rafforzare la fiducia.
   • Per i casi Sconosciuto, il sistema categorizza quali elementi sono ambigui o indefiniti, distinguendo le vere contraddizioni dai comportamenti sottodeterminati.

4. Metrica Quantitativa:

   • Il framework definisce un Punteggio di Allineamento ($a_t$) calcolato come il rapporto tra le asserzioni che implicano ($E$) e il numero totale di asserzioni ($n$) a una data iterazione ($a_t = E/n$). L'obiettivo del processo di raffinamento è massimizzare questo punteggio.

C. Estrazione del Riassunto in Linguaggio Naturale

Una fase critica di pre-elaborazione consiste nella conversione delle SVA formali in riassunti strutturati in linguaggio naturale. L'LLM viene sollecitato a identificare componenti specifici delle SVA (Trigger, Antecedente, Operatore di Implicazione, Conseguente e Disable If) e a mapparli su frasi equivalenti in linguaggio naturale. Ciò garantisce che l'intento semantico del codice formale sia preservato per il confronto.

3. Contributi Chiave

Il documento delinea i seguenti contributi:

• Framework di Valutazione Semantica: Un approccio innovativo per valutare le SVA generate da LLM rispetto a specifiche in linguaggio naturale senza fare affidamento sulla verifica formale applicata a un RTL golden.
• Pipeline di Raffinamento Iterativo: Un framework strutturato composto da Controllo di Allineamento, Analisi delle Incoerenze ed Estrazione del Riassunto delle SVA, progettato per l'integrazione nei flussi di lavoro esistenti basati su LLM.
• Metrica Quantitativa di Allineamento: Una metrica di punteggio di allineamento basata sulla classificazione dell'implicazione semantica per misurare la coerenza con la specifica, offrendo un'alternativa scalabile alla tradizionale valutazione della correttezza FV.
• Meccanismo di Analisi delle Incoerenze: Un metodo per generare feedback specifici e azionabili per proprietà e asserzioni contraddittorie, a supporto sia della revisione manuale che del raffinamento automatizzato.
• Validazione Empirica: Risultati sperimentali che dimostrano la riduzione delle asserzioni contraddittorie nei progetti APB e UART attraverso il raffinamento semantico.

4. Risultati Sperimentali

Gli autori hanno valutato SpecAlign su due progetti hardware: APB (Interfaccia da APB a I2C) e UART (Interfaccia da UART a Bus). Il framework è stato confrontato con AssertionForge, un metodo di base che utilizza un grafo della conoscenza e incorpora l'RTL nella generazione.

• Risultati APB:
  • Base (AssertionForge): Ha generato 442 SVA con un punteggio di allineamento di 0,02. Solo 8 erano implicanti, mentre 148 erano contraddittorie.
  • SpecAlign: Ha mantenuto 442 SVA ma ha aumentato il punteggio di allineamento a 0,15. Crucialmente, il numero di asserzioni contraddittorie è sceso a 0, con 66 asserzioni implicanti. Le rimanenti 376 sono state classificate come Sconosciute.
• Risultati UART:
  • Base: Ha generato 325 SVA con un punteggio di allineamento di 0,06 (21 implicanti, 142 contraddittorie).
  • SpecAlign: Ha generato 319 SVA con un punteggio di allineamento di 0,28. Le asserzioni contraddittorie sono state ridotte a 6, mentre le asserzioni implicanti sono aumentate a 92.

Analisi dei Risultati:
Gli esperimenti hanno rivelato che i metodi di base generano spesso asserzioni che sono o contraddittorie rispetto alla specifica o che fanno molto affidamento su dettagli specifici dell'implementazione (RTL) non presenti nella specifica in linguaggio naturale. SpecAlign filtra efficacemente queste contraddizioni. L'aumento delle classificazioni "Sconosciuto" in SpecAlign (ad esempio, 376 per APB) è interpretato non come un fallimento, ma come una strategia di classificazione più conservativa e accurata che separa le assunzioni specifiche dell'implementazione dal comportamento supportato dalla specifica. Questa distinzione previene l'etichettatura come "implicanti" di comportamenti non supportati (falsi positivi).

5. Significato e Affermazioni

Il documento afferma che SpecAlign fornisce un complemento scalabile alla verifica formale tradizionale. Separando la correttezza semantica dai risultati della prova RTL, affronta il limite secondo cui la sola verifica formale non può determinare se un'asserzione cattura il comportamento inteso descritto nella specifica.

Gli autori sottolineano che, sebbene la verifica formale sia necessaria per dimostrare che le asserzioni valgono sull'RTL, è insufficiente per valutare la qualità dell'intento dell'asserzione. SpecAlign migliora la fiducia nelle asserzioni generate da LLM:

1. Rilevando incoerenze semantiche che gli strumenti formali potrebbero perdere (ad esempio, verità vuote).
2. Riducendo gli sforzi di debug identificando le contraddizioni prima della simulazione RTL o della prova formale.
3. Fornendo un meccanismo per raffinare le asserzioni in modo iterativo senza richiedere un modello golden.

Il documento conclude con modestia, notando che, sebbene il framework migliori l'allineamento, sono necessari lavori futuri per affinare le metodologie di classificazione, catturare meglio gli errori sintattici ed estendere l'approccio ad altri compiti di automazione della progettazione hardware come la generazione e il debug RTL.