QiMeng-CodeV-SVA: Training Specialized LLMs for Hardware Assertion Generation via RTL-Grounded Bidirectional Data Synthesis

Il paper presenta QiMeng-CodeV-SVA, un framework di sintesi dati bidirezionale che sfrutta RTL open-source per addestrare modelli LLM specializzati nella generazione di asserzioni SystemVerilog, ottenendo prestazioni superiori rispetto a modelli avanzati come GPT-5 e DeepSeek-R1.

L'essenziale

Immagina di dover costruire un orologio meccanico estremamente complesso. Per assicurarti che funzioni perfettamente, hai bisogno di un manuale di istruzioni (il codice RTL) e di una lista di regole di controllo (le "Assertion" o SVA) che dicano: "Se l'ingranaggio A gira, allora l'ingranaggio B deve fermarsi".

Se queste regole sono sbagliate, l'orologio si rompe o, peggio, sembra funzionare ma in realtà non lo fa. Scrivere queste regole a mano è un lavoro da esperti, lento e costoso.

Ecco la storia di QiMeng-CodeV-SVA, un progetto che ha insegnato a un'intelligenza artificiale a scrivere queste regole da sola, in modo perfetto.

1. Il Problema: Troppi progetti, poche regole

Gli scienziati volevano usare l'Intelligenza Artificiale (come ChatGPT) per scrivere queste regole di controllo. Ma c'era un grosso ostacolo: mancavano i libri di testo.

• Non c'erano abbastanza esempi reali di "Progetto + Regola Corretta" per addestrare l'AI.
• Le poche regole che esistevano erano poche e spesso confuse.
• Inoltre, come fai a sapere se l'AI ha scritto una regola giusta? Se chiedi all'AI stessa "è giusta?", potrebbe mentire o confondersi.

2. La Soluzione: La "Fabbrica di Regole" (Sintesi dei Dati)

Invece di cercare disperatamente regole esistenti, i ricercatori hanno deciso di crearle loro stessi partendo dai progetti reali.

Immagina di avere una biblioteca piena di progetti di orologi (codice RTL open source).

1. L'Architetto (LLM): Prende un progetto e dice: "Ok, questo orologio ha un contatore. Dovrebbe avere una regola che dice 'se il contatore è attivo, deve aumentare'".
2. Il Controllore di Qualità (Strumento Formale): Prende questa nuova regola e la testa contro il progetto reale. Se la regola regge e non crea errori, viene salvata. Se è una sciocchezza (es. "il sole è caldo"), viene scartata.

In questo modo, hanno creato un enorme manuale di istruzioni (83.000 esempi) partendo dal nulla, usando i progetti reali come base.

3. Il Trucco Magico: La "Traduzione a Specchio" (Bidirectional Translation)

Qui arriva la parte più geniale. Come fanno a essere sicuri che la regola scritta dall'AI corrisponda esattamente a ciò che l'ingegnere umano voleva dire?

Hanno usato un metodo che chiamiamo "Traduzione a Specchio":

• Passo 1: L'AI prende la regola tecnica (SVA) e la traduce in linguaggio semplice (es. "Il contatore deve salire").
• Passo 2: L'AI prende quella frase semplice e la riscrive di nuovo in linguaggio tecnico.
• Il Test: Se la nuova versione tecnica è identica (o logicamente equivalente) alla prima, allora la regola è perfetta!
• Se non è identica: Significa che c'è stato un errore di traduzione o di comprensione. La regola viene buttata via.

È come se tu dicessi a un amico: "Traduci questa frase in francese e poi tornala a tradurre in italiano". Se la frase finale è diversa da quella originale, sai che qualcosa è andato storto nel mezzo. Questo metodo ha pulito i dati, eliminando gli errori sottili che nemmeno gli strumenti di verifica tradizionali vedevano.

4. Il Risultato: Il "Maestro" (CodeV-SVA)

Dopo aver addestrato l'AI con questi dati "puliti" e verificati, hanno creato CodeV-SVA.

I risultati sono stati sbalorditivi:

• Questo modello, anche se più piccolo ed economico di giganti come GPT-5, è diventato il migliore al mondo nel compito specifico di scrivere regole per l'hardware.
• Ha superato i modelli generalisti più famosi, dimostrando che non serve essere il più grande, ma essere il più specializzato.

In sintesi

I ricercatori hanno risolto il problema della scarsità di dati non cercando più dati, ma costruendo la loro propria scuola di addestramento.
Hanno usato i progetti reali come "palestra", un sistema di "traduzione a specchio" come "ispettore severo" per eliminare gli errori, e hanno creato un modello AI che oggi è in grado di scrivere le regole di sicurezza per i chip elettronici meglio di qualsiasi esperto umano o AI generica.

È come se avessero insegnato a un apprendista orologiaio non solo a guardare i manuali, ma a costruire migliaia di orologi di prova, a correggere i propri errori da solo e a diventare il maestro definitivo.

Sommario tecnico

1. Il Problema

La verifica formale dell'hardware basato su asserzioni (SystemVerilog Assertions - SVA) è fondamentale nel flusso di progettazione digitale. Tuttavia, la creazione manuale di SVAs di alta qualità richiede un enorme sforzo e competenze specializzate.
L'uso di Modelli Linguistici su larga scala (LLM) generici per tradurre specifiche in linguaggio naturale (NL) in SVAs (compito NL2SVA) ha mostrato risultati deludenti a causa di due sfide principali:

1. Scarsità di dati di addestramento: Esiste una carenza di corpora reali di alta qualità che accoppiano proprietà in linguaggio naturale con SVAs corrispondenti. I dataset pubblici sono limitati (spesso tratti da libri di testo o repository open-source frammentati) e non scalano come i dati RTL (Register Transfer Level).
2. Mancanza di metodi di validazione affidabili: È difficile determinare automaticamente l'equivalenza semantica tra una proprietà in linguaggio naturale e un SVA generato.
   • Gli strumenti di verifica formale (es. JasperGold) da soli non bastano: un SVA banale (es. assert property (1'b1)) passa la verifica su qualsiasi RTL ma non corrisponde alla specifica naturale.
   • L'approccio "LLM-as-a-judge" fallisce spesso a causa dell'ambiguità del linguaggio naturale e della sintassi complessa degli SVA (es. priorità degli operatori).

2. Metodologia: Il Framework di Sintesi Dati

Gli autori propongono un framework di sintesi dati innovativo per addestrare LLM specializzati, composto da quattro fasi principali:

A. Sintesi SVA basata su RTL Reale (RTL-Grounded Synthesis)

Invece di affidarsi a dati esistenti, il framework utilizza grandi quantità di codice RTL open-source (dal dataset CodeV) come "Design Under Test" (DUT).

• Un LLM generico analizza le specifiche e il codice RTL per generare molteplici proprietà in linguaggio naturale e i relativi candidati SVA.
• Gli SVA generati vengono filtrati tramite strumenti di verifica formale (JasperGold) per garantire che siano verificabili sul codice RTL specifico. Questo produce un dataset iniziale di alta qualità (159K istanze).

B. Selezione Bidirezionale (Bidirectional Selection)

Questa è la componente chiave per garantire la coerenza semantica. Il processo funziona come segue:

1. Traduzione SVA $\to$ NL: Un SVA verificato viene tradotto indietro in linguaggio naturale da un LLM.
2. Traduzione NL $\to$ SVA: La nuova descrizione in linguaggio naturale viene riconvertita in un nuovo SVA.
3. Controllo di Equivalenza: Lo strumento di verifica formale controlla se il nuovo SVA è logicamente equivalente all'SVA originale.
   • Se sono equivalenti, la coppia (NL, SVA) è ritenuta coerente e viene mantenuta.
   • Se non sono equivalenti, indica una perdita di informazione o un errore di sintesi (es. un SVA che "imbrogliava" la verifica ma non catturava la logica reale) e viene scartato.
   • Risultato: Questo metodo riduce il dataset a 105K coppie, ma con una qualità semantica molto superiore.

C. Affinamento della Qualità dei Dati

Ulteriori tecniche per migliorare il dataset:

• LLM-as-a-judge con esperti: Filtraggio di errori specifici (allineamento logico, incoerenza dei segnali) identificati da esperti umani.
• Filtraggio della Difficoltà: Rimozione di dati banali dove anche modelli deboli riescono a generare SVAs corretti.
• Augmentation delle Traiettorie di Ragionamento: Utilizzo di un modello di ragionamento avanzato (DeepSeek-R1) per generare percorsi di ragionamento (chain-of-thought) prima della risposta finale, migliorando la capacità di inferenza del modello.

D. Addestramento Supervisionato (SFT)

I modelli base open-source (Qwen3 8B e 14B) vengono addestrati (Fine-Tuning) sul dataset sintetizzato finale di 83K istanze, utilizzando il formato di ragionamento di DeepSeek-R1.

3. Contributi Chiave

1. Framework di Sintesi Dati RTL-Grounded: Una metodologia scalabile per generare dataset NL-SVA di alta qualità partendo da codice RTL reale, superando il collo di bottiglia della scarsità di dati.
2. Selezione Bidirezionale: Un metodo robusto e automatico per validare l'allineamento semantico tra linguaggio naturale e asserzioni hardware, risolvendo il problema della validazione automatica in questo dominio.
3. CodeV-SVA: Una serie di modelli LLM specializzati (8B e 14B) che dimostrano come l'addestramento su dati sintetizzati di alta qualità possa superare i modelli generici molto più grandi.

4. Risultati Sperimentali

I modelli CodeV-SVA sono stati valutati sui benchmark FVEval-NL2SVA (Human e Machine).

• Prestazioni Superiori:

  • CodeV-SVA-14B ha raggiunto il 75.8% di accuratezza (Func.@1) su NL2SVA-Human e l'84.0% su NL2SVA-Machine.
  • Questi risultati superano o eguagliano modelli generici di stato dell'arte (SOTA) molto più grandi e costosi, come GPT-5 e DeepSeek-R1 (671B), pur essendo modelli open-source molto più piccoli ed economici da distribuire.
  • I modelli CodeV-SVA hanno mostrato un miglioramento significativo rispetto alle loro versioni base (Qwen3), confermando che la qualità dei dati sintetizzati è il fattore determinante.

• Studi di Ablazione:

  • La Selezione Bidirezionale ha contribuito al guadagno di prestazioni più sostanziale (circa +12% su NL2SVA-Human), dimostrando la sua efficacia nel filtrare errori sottili.
  • L'uso di dati sintetizzati da LLM ha superato di gran lunga l'uso di dati raccolti da repository open-source o riscritti con regole.
  • L'aggiunta di traiettorie di ragionamento ha migliorato ulteriormente le prestazioni.

• Verifica End-to-End:

  • In un flusso di verifica automatizzato (basato su AssertionForge), CodeV-SVA ha generato un numero significativamente maggiore di SVAs corretti sintatticamente e verificabili formalmente rispetto a GPT-4o e DeepSeek-R1, specialmente su design complessi (es. OPENMSP430).

5. Significato e Impatto

Questo lavoro rappresenta un passo avanti cruciale nell'uso dell'IA per l'EDA (Electronic Design Automation):

• Democratizzazione della Verifica Hardware: Dimostra che non è necessario possedere modelli proprietari giganti o costosi per compiti di verifica hardware specializzati; è sufficiente un modello open-source addestrato su dati sintetizzati di alta qualità.
• Soluzione al Problema dei Dati: Offre una soluzione pratica alla carenza di dati etichettati nel settore hardware, trasformando il codice RTL (abbondante) in dati di addestramento per la verifica.
• Affidabilità: Il metodo di selezione bidirezionale fornisce un nuovo standard per la validazione automatica della coerenza semantica in compiti di traduzione tecnica complessa.

In sintesi, QiMeng-CodeV-SVA stabilisce un nuovo stato dell'arte per la generazione automatica di asserzioni hardware, combinando sintesi dati su larga scala, validazione rigorosa e addestramento specializzato.