Riepilogo Tecnico: CktFormalizer

Enunciato del Problema

La progettazione hardware rimane una disciplina soggetta a errori, in cui difetti sottili, come mismatch di larghezza dei bit, loop combinatori o logica di caso incompleta nelle Macchine a Stati Finiti (FSM), possono superare i controlli di sintassi ma fallire silenziosamente durante la sintesi o manifestarsi come bug costosi nel silicio in fasi successive. Sebbene i Modelli Linguistici di grandi dimensioni (LLM) abbiano dimostrato la capacità di generare Verilog a partire da specifiche in linguaggio naturale, il codice risultante eredita spesso le insidie intrinseche di Verilog e VHDL: una mancanza di garanzie statiche come tipi dipendenti, matching di pattern esaustivo e prove verificate dalla macchina. Di conseguenza, l'hardware generato dagli LLM richiede frequentemente un'ampia attività di debug manuale e spesso non riesce a raggiungere l'implementazione fisica (Place-and-Route, DRC, LVS), anche quando è funzionalmente corretto nella simulazione.

Metodologia

Il documento presenta CktFormalizer, un framework che unisce la generazione di codice guidata dagli LLM alla verifica formale, mirando a un Linguaggio di Descrizione Hardware (HDL) con tipi dipendenti incorporato in Lean 4. Invece di generare direttamente Verilog, il sistema reindirizza l'agente LLM a generare codice Lean, che funge da target principale di compilazione.

Architettura Principale

Il framework opera attraverso una pipeline a ciclo chiuso che coinvolge tre ruoli distinti per Lean:

1. Type Checker (Verificatore a Tempo di Compilazione): Il sistema di tipi dipendenti di Lean codifica i vincoli di larghezza dei bit, la copertura dei casi e l'aciclicità. I difetti hardware (ad esempio, mismatch di larghezza o loop combinatori) vengono rilevati come errori di tipo a tempo di compilazione anziché come fallimenti silenziosi del backend. Ciò fornisce all'agente LLM un feedback immediato e azionabile per riparare iterativamente il progetto.
2. Firewall di Correttezza: I progetti che compilano con successo in Lean sono strutturalmente garantiti come privi di specifiche classi di difetti (mismatch di larghezza, loop combinatori, latch non intenzionali). Ciò garantisce che i progetti compilati sopravvivano al flusso di sintesi backend e Place-and-Route (P&R) senza il tasso di perdita del 20% osservato nella generazione di Verilog di base.
3. Assistente di Prova: L'agente costruisce prove di teoremi automatizzate per verificare l'equivalenza funzionale tra la specifica in linguaggio naturale e l'implementazione generata (o ottimizzata). Queste prove coprono sequenze di input arbitrarie e larghezze parametriche, andando oltre i limiti del controllo basato su SMT limitato.

Flusso di Lavoro

1. Generazione e Iterazione: Un agente LLM (istanziato con Claude) genera codice HDL in Lean basato su una specifica in linguaggio naturale. Entra in un ciclo iterativo "genera-compila-ripara" in cui gli errori del compilatore Lean guidano l'agente a correggere i bug semantici prima che si propaghino.
2. Estrazione: Al termine di una compilazione riuscita, un metaprogramma (#synthesizeVerilog) estrae SystemVerilog sintetizzabile dal grafo dei combinatori di segnale Lean.
3. Implementazione Fisica: Il SystemVerilog estratto viene simulato, sintetizzato (utilizzando Yosys) e implementato fisicamente (utilizzando OpenROAD con il PDK SkyWater 130nm) per generare layout GDSII e metriche Power-Performance-Area (PPA).
4. Ciclo di Ottimizzazione PPA: Una fase di ottimizzazione a ciclo chiuso reinvia le metriche PPA all'agente. L'agente propone varianti architetturali (ad esempio, percorsi dati paralleli vs. seriali) e deve fornire prove di equivalenza verificate dalla macchina per garantire che la variante ottimizzata rimanga funzionalmente equivalente alla specifica originale.

Contributi Chiave

1. Primo Framework End-to-End: CktFormalizer è il primo framework a combinare la generazione hardware guidata dagli LLM con un HDL incorporato in Lean, fornendo una pipeline dal linguaggio naturale al silicio sintetizzabile con ottimizzazione PPA a ciclo chiuso.
2. Generazione Guidata dai Tipi: Il documento dimostra che mirare a un HDL sicuro per i tipi migliora sostanzialmente i tassi di successo degli LLM rispetto alla generazione diretta di Verilog. Gli errori di tipo a tempo di compilazione forniscono un feedback strutturato che guida l'agente verso progetti corretti, scalando fino a IP rilevanti per l'industria come interfacce di bus di handshake multicanale.
3. Integrazione della Verifica Formale: Il framework colma il divario tra il codice generato dagli LLM e l'hardware provatamente corretto permettendo all'agente di produrre prove di equivalenza verificate dalla macchina. Ciò garantisce che le ottimizzazioni architetturali non compromettano la correttezza funzionale.

Risultati Sperimentali

Il framework è stato valutato su tre benchmark: VerilogEval (156 problemi), RTLLM (50 problemi) e ResBench (56 problemi).

• Realizzabilità Backend: Una scoperta critica è che CktFormalizer preserva la correttezza funzionale attraverso il backend. Mentre la baseline (generazione diretta di Verilog) perde circa il 20% dei progetti funzionalmente corretti durante la sintesi e il routing, CktFormalizer preserva il 100% dei suoi progetti compilati attraverso l'intero flusso di sintesi, P&R, DRC e LVS.
• Compilazione e Simulazione: Su VerilogEval, CktFormalizer ha raggiunto un tasso di compilazione Lean del 92,3% e un tasso di superamento della simulazione RTL del 72,4%, risultati competitivi rispetto alle baseline di generazione diretta di Verilog. Quando il feedback di sintesi è incluso nel ciclo dell'agente, il tasso di compilazione sale al 99,4%.
• Ottimizzazione PPA: La fase di ottimizzazione a ciclo chiuso ha prodotto miglioramenti significativi. Attraverso l'esplorazione architetturale validata, il framework ha raggiunto una riduzione dell'area fino al 35% e una riduzione della potenza fino al 30%.
• Chiusura Temporale: Tutti i progetti funzionalmente corretti che hanno completato Place-and-Route hanno raggiunto la chiusura temporale (WNS $\ge$ 0 ns) senza intervento manuale.
• Generazione di Prove: In uno studio pilota, la generazione di prove passo dopo passo (rifinitura iterativa con feedback sugli obiettivi di prova) ha migliorato i tassi di completamento delle prove dal 53% al 63%, dimostrando la fattibilità degli assistenti di prova per la verifica hardware.

Significato e Affermazioni

Il documento afferma che i tipi dipendenti e gli agenti LLM sono complementari. Utilizzando un linguaggio formale (Lean) sia come target di generazione che come substrato di verifica, il framework trasforma il ciclo "genera-e-testa" dell'LLM da una ricerca stocastica su programmi sintatticamente validi in un processo di raffinamento guidato dai tipi.

Gli autori sottolineano che il compilatore agisce come verificatore, spostando il rilevamento degli errori dalla fine della pipeline EDA (dove le correzioni sono costose) al momento della compilazione. Questo approccio permette al sistema di produrre hardware che non è solo funzionalmente corretto, ma anche strutturalmente robusto contro le trasformazioni backend, risolvendo efficacemente il problema del "fallimento silenzioso" comune nell'hardware generato dagli LLM. Il lavoro suggerisce che i linguaggi formali possono servire come fondamento per una progettazione hardware automatizzata e affidabile, permettendo agli LLM di navigare i complessi compromessi dell'ottimizzazione hardware mantenendo rigorose garanzie di correttezza.