Riepilogo Tecnico: VERI-SURE

1. Definizione del Problema

Il deployment di Large Language Models (LLM) per la progettazione di Register-Transfer Level (RTL) nell'Electronic Design Automation (EDA) affronta ostacoli significativi nel raggiungere una correttezza di grado siliconico (silicon-grade). Sebbene gli LLM abbiano fatto progressi nella generazione di codice software, la generazione RTL presenta sfide uniche a causa della natura concorrente dell'hardware, del rigoroso timing a livello di ciclo e della semantica dei protocolli. Il documento identifica tre colli di bottiglia primari nelle attuali pipeline RTL basate su LLM:

1. Affidabilità della Valutazione Limitata: Le valutazioni incentrate sulla simulazione soffrono spesso di una copertura dei test insufficiente, fallendo nel rilevare sottili casi limite temporali (corner cases).
2. Inefficienze nel Debugging: Il debugging iterativo porta spesso a "regressioni e allucinazioni di riparazione" causate dalla rigenerazione dell'intero file, il che destabilizza la logica non correlata.
3. Deriva Semantica (Semantic Drift): Man mano che l'intento in linguaggio naturale viene reinterpretato attraverso molteplici passaggi tra agenti o iterazioni, l'intento di progettazione originale può degradare, portando a implementazioni incoerenti.

I benchmark esistenti, come VerilogEval-v2, sono criticati perché dominati da moduli brevi e pedagogici che non rappresentano adeguatamente le necessità industriali, quali unità aritmetiche avanzate, protocolli di comunicazione e pattern di Clock Domain Crossing (CDC).

2. Metodologia: Il Framework VERI-SURE

VERI-SURE è un framework multi-agente consapevole dei contratti (contract-aware), progettato per chiudere il ciclo tra sintesi del codice, verifica e riparazione localizzata. Si sposta oltre la traduzione "one-shot" verso un ciclo automatizzato di generazione-verifica-debugging.

Componenti Core

• Design Contract (Agente Architetto): Il framework inizia distillando le specifiche in linguaggio naturale in un contratto di progettazione strutturato in formato JSON. Questo contratto definisce esplicitamente la semantica delle interfacce, le convenzioni di clock/reset, il comportamento accurato al ciclo e i casi limite. Serve come "fonte di verità" condivisa per tutti gli agenti successivi per prevenire la deriva semantica.
• Workflow Multi-Agente:
  • Agente Coder: Genera codice RTL sintetizzabile basato sul contratto.
  • Agente Verifier: Produce testbench auto-verificanti allineati al contratto.
  • Agente Debugger: Guida il ciclo di debugging autonomo quando la simulazione fallisce.
  • Agente Asserter: Genera asserzioni SystemVerilog mirate per rilevare violazioni sequenziali o di protocollo (ad esempio, campionamento sul fronte errato, mismatch del reset).
  • Agente Boolean Proofer: Esegue la verifica formale sulla logica combinatoria per validare le correzioni candidate e prevenire regressioni.

Meccanismi Chiave

• Analisi Temporale Guidata da Tracce e Slicing Statico: Quando la simulazione fallisce, il sistema non si affida esclusivamente ai log testuali. Analizza le forme d'onda Value Change Dump (VCD) per identificare il tempo di divergenza iniziale ($t_f$). Successivamente, impiega lo slicing di dipendenza statica per calcolare il "cono di logica" che influenza i segnali in errore. Questo isola il fallimento a un set minimo di blocchi di codice sospetti (intervalli di righe), piuttosto che all'intero file.
• Patching Localizzato: Guidato dall'analisi di slicing, l'agente Debugger applica modifiche precise a livello di blocco (leggi/sostituisci) solo ai blocchi sospetti. Ciò evita l'instabilità delle riscritture dell'intero file. Una regola di rollback assicura che le patch siano mantenute solo se migliorano la firma del fallimento (ad esempio, un tempo di primo fallimento più tardivo o meno mismatch).
• Verifica Multi-Branch: Il framework integra due rami di verifica:
  1. Analisi Temporale Guidata da Traccia: Per problemi sequenziali e di timing.
  2. Verifica Formale: Combina il controllo basato su asserzioni (tramite l'Asserter) e prove di equivalenza booleana (tramite il Boolean Proofer usando SymbiYosus) per verificare i vincoli combinatori e provare la correttezza oltre la simulazione finita.

3. Benchmark: VERILOGEVAL-V2-EXT

Per valutare meglio la generazione RTL di grado industriale, gli autori introducono VERILOGEVAL-V2-EXT. Questo benchmark estende l'originale VerilogEval-v2 aggiungendo 53 nuovi task di progettazione di grado industriale, portando il totale a 209 problemi.

• Contenuto: I nuovi task coprono domini complessi come protocolli di comunicazione (UART, FIFO), aritmetica avanzata, kernel DSP e datapath multi-ciclo.
• Stratificazione: I problemi sono classificati in livelli di difficoltà Easy, Medium e Hard basandosi sui segnali strutturali (righe di codice, numero di blocchi assign/always, larghezza del datapath) e revisione manuale. Ciò consente un'analisi più fine delle modalità di fallimento.

4. Risultati Sperimentali

Gli autori hanno valutato VERI-SURE contro 15 LLM standalone (inclusi modelli commerciali a codice chiuso e modelli open-weight), cicli di feedback a singolo agente e precedenti sistemi multi-agente (MAGE, VerilogCoder).

• Performance: VERI-SURE ha raggiunto uno stato dell'arte del 93,30% di Pass@1 funzionale sul benchmark VERILOGEVAL-V2-EXT, con il 100% di successo nella sintassi.
• Task Difficili (Hard): Il framework ha mostrato il suo maggiore vantaggio sui task "Hard", raggiungendo un tasso di successo funzionale dell'85,07%, superando significativamente il miglior modello standalone (Gemini-3-Pro al 62,69%) e altri baseline agentici.
• Agnosticismo del Backbone: Sebbene VERI-SURE abbia performato meglio con GPT-5.2, ha anche incrementato significativamente le prestazioni del modello open-weight DeepSeek-3.2, elevando il suo tasso di successo funzionale dal 61,24% (standalone) al 71,29%.
• Studi di Ablazione:
  • Rimuovere il meccanismo di Tracing, Slicing e Patching ha causato il calo di performance più grande (11,0% complessivo, 16,4% sui task Hard), confermando che la localizzazione precisa è critica.
  • Rimuovere la Verifica Formale ha ridotto il tasso di successo dei task Hard di 11,9 punti percentuali, dimostrando la sua necessità per il debugging di bug logici profondi che la simulazione perde.
  • Il meccanismo del Contract ha contribuito a un calo del 2,9% delle performance complessive quando rimosso, evidenziando il suo ruolo nel mantenere la coerenza dell'intento.

5. Significato e Claim

Il documento sostiene che VERI-SURE dimostra che la progettazione RTL automatizzata può avvicinarsi alla "correttezza di grado siliconico" spostandosi da una valutazione centrata sulla simulazione a un approccio ibrido che combina l'analisi guidata da tracce e la verifica formale.

I claim principali includono:

• Mitigazione della Deriva Semantica: Imponendo un contratto di progettazione strutturato, il framework allinea gli intenti degli agenti e previene la graduale reinterpretazione dei requisiti.
• Stabilità nella Riparazione: Il meccanismo di patching guidato dallo slicing di dipendenza riduce efficacemente i rischi di regressione e le allucinazioni di riparazione associate alla rigenerazione dell'intero file.
• Oltre la Simulazione: L'integrazione di prove formali permette al sistema di verificare la correttezza funzionale in modi in cui la pura simulazione non può, in particolare per l'equivalenza combinatoria e i vincoli di timing complessi.
• Rilevanza Industriale: L'introduzione di VERILOGEVAL-V2-EXT fornisce un testbed più realistico e discriminante per valutare le capacità di generazione RTL end-to-end, colmando il divario tra i benchmark accademici e i requisiti dei blocchi IP industriali.

Gli autori concludono che, sebbene il pre-training su larga scala fornisca una base solida, il workflow agentico strutturato con verifica formale è essenziale per raggiungere un'alta affidabilità nei complessi design hardware multi-ciclo.