💻 computer science

From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation

Il paper presenta **ProofLoop**, un agente basato su LLM che automatizza la generazione di asserzioni SystemVerilog (SVA) partendo da specifiche in linguaggio naturale, utilizzando un approccio "solver-in-the-loop" che integra strumenti EDA e cicli di raffinamento iterativo per garantire elevata correttezza sintattica e funzionale.

Autori originali: Nowfel Mashnoor, Hadi Kamali, Kimia Azar

Pubblicato 2026-04-28

📖 3 min di lettura☕ Lettura da pausa caffè

CC BY 4.0

Autori originali: Nowfel Mashnoor, Hadi Kamali, Kimia Azar

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Il Problema: Il "Traduttore" che non conosce il Progetto

Immagina di dover spiegare a un assistente robotico come deve comportarsi un complesso sistema di ingranaggi in una fabbrica. Tu gli dai un foglio con scritto in linguaggio naturale: "Assicurati che la valvola si chiuda sempre se la pressione sale troppo velocemente".

Il problema è che il robot è molto intelligente con le parole, ma non ha mai visto la fabbrica. Non sa dove si trova la valvola, non sa quale interruttore aziona la pressione e non sa se la valvola si chiude istantaneamente o se ci mette due secondi. Se gli dai istruzioni imprecise, lui scriverà un manuale di regole (che in gergo tecnico si chiamano SVA - SystemVerilog Assertions) che è pieno di errori: userà nomi di pezzi che non esistono o darà regole che violano le leggi della fisica della fabbrica.

In breve: i modelli di intelligenza artificiale (LLM) sono ottimi scrittori, ma pessimi ingegneri perché "non vedono" l'hardware che devono controllare.

La Soluzione: ProofLoop (L'Ingegnere con la Lente d'Ingrandimento)

I ricercatori hanno creato ProofLoop. Non è solo un chatbot, è un "Agente Investigatore". Invece di limitarsi a leggere il tuo comando e scrivere subito le regole, ProofLoop lavora in due fasi, proprio come un vero ingegnere:

Fase A: L'Investigazione (Il Detective)

Invece di tirare a indovinare, l'agente inizia a esplorare la fabbrica. Usa degli strumenti speciali (chiamati RAG e strumenti strutturali) per:

Cercare nei manuali: "Dove sono i cavi della pressione?"
Esaminare i pezzi: "Questa valvola è collegata a un interruttore o a un sensore?"
Mappare la struttura: "Se premo questo, cosa succede in quella stanza lontana?"

È come se, prima di scrivere il regolamento, l'assistente facesse un giro completo in fabbrica con una torcia e una mappa, prendendo appunti su ogni singolo bullone.

Fase B: Il Ciclo di Correzione (L'Apprendista e il Maestro)

Una volta raccolte le informazioni, l'agente scrive le regole. Ma non si ferma qui. Passa le regole a un "Maestro Severo" (un software chiamato JasperGold, che è un verificatore formale).

Il Maestro non dice solo "va bene" o "va male". Se la regola è sbagliata, il Maestro dice: "Ehi, hai scritto che la valvola si chiude con l'interruttore A, ma in realtà è collegata all'interruttore B!".

L'agente riceve questa critica, torna sui suoi appunti, corregge l'errore e riprova. Questo processo si ripete finché la regola non è perfetta e matematicamente dimostrata. È un ciclo di apprendimento continuo (chiamato Solver-in-the-loop).

Perché è una rivoluzione? (I Risultati)

I ricercatori hanno testato ProofLoop su una serie di "esami" difficili (il benchmark FVEval) e i risultati sono stati impressionanti:

Precisione quasi perfetta: Mentre un'IA normale farebbe un sacco di errori di "grammatica" tecnica, ProofLoop ne sbaglia pochissimi (oltre il 93% delle regole sono scritte correttamente).
Capacità di risolvere problemi complessi: Più la "fabbrica" (il design hardware) diventa grande e complicata, più ProofLoop diventa bravo rispetto alle IA normali, che invece vanno in confusione.
Impara dai propri errori: Grazie al feedback del "Maestro", l'IA riesce a correggere i propri sbagli invece di ripetere lo stesso errore all'infinito.

In sintesi

ProofLoop trasforma l'IA da un semplice "scrittore di testi" a un "ingegnere assistente" che sa esplorare il progetto, studiare i componenti e imparare dai propri errori matematici, rendendo la creazione di regole di sicurezza per i chip elettronici molto più veloce e affidabile.

Riassunto Tecnico: "From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation"

1. Il Problema (Problem Statement)

La verifica basata su asserzioni (Assertion-Based Verification, ABV) è fondamentale per il design di hardware digitale, ma la creazione manuale di SystemVerilog Assertions (SVA) è un compito estremamente complesso. Richiede una profonda conoscenza sia della semantica del codice RTL (Register-Transfer Level) sia della logica temporale.

Sebbene i Large Language Models (LLM) siano stati utilizzati per automatizzare questo processo, gli approcci esistenti presentano tre limiti critici:

Riferimenti errati ai segnali: Gli LLM spesso inventano nomi di segnali o non comprendono la gerarchia del design.
Mancanza di contesto strutturale: Gli LLM non hanno accesso a metadati hardware cruciali (es. domini di clock, tipi di reset, relazioni fan-in/fan-out).
Assenza di garanzie formali: Le asserzioni generate spesso falliscono la compilazione o non sono funzionalmente corrette rispetto al comportamento reale dell'hardware.

2. Metodologia (Methodology: ProofLoop)

Per superare questi limiti, gli autori propongono ProofLoop, un agente basato sul framework ReAct (Reasoning + Acting) che integra un approccio "solver-in-the-loop" utilizzando lo strumento EDA Cadence JasperGold. Il sistema opera in tre fasi principali:

Fase di Indicizzazione AST: Il codice RTL viene analizzato tramite un compilatore SystemVerilog per generare un Abstract Syntax Tree (AST). Il design viene scomposto in "chunk" semantici (interfacce di moduli, blocchi always, istanze, assegnazioni continue) e memorizzato in un database vettoriale per consentire la ricerca semantica (RAG - Retrieval-Augmented Generation).
Fase A - Raccolta del Contesto (Agentic Context Synthesis): L'agente non segue un percorso fisso, ma decide autonomamente quali strumenti invocare attraverso un ciclo di ragionamento (Thought $\rightarrow$ Action $\rightarrow$ Observation). Utilizza:
- Strumenti di Retrieval: Per interrogare il database vettoriale e trovare frammenti di codice rilevanti.
- Strumenti di Analisi Strutturale (JasperGold): Per estrarre metadati hardware come la dipendenza dei segnali e le proprietà dei flip-flop (clock e reset).
Fase B - Generazione e Ciclo di Raffinamento (Solver-in-the-Loop): L'agente genera le SVA e le sottopone a JasperGold. Se l'asserzione fallisce (errore di sintassi, falsificazione o vacuità), il feedback del solver (messaggi di errore e controesempi) viene reimmesso nell'agente, che esegue modifiche mirate per correggere l'asserzione invece di rigenerarla da zero.

3. Contributi Chiave (Key Contributions)

Sintesi del contesto agentica: Un sistema che raccoglie autonomamente informazioni rilevanti per la verifica tramite ricerca semantica e query strutturali.
Raffinamento iterativo tramite solver: Un ciclo di feedback che utilizza i risultati della verifica formale per riparare sintassi e logica temporale.
Scalabilità: Un framework capace di gestire design complessi e multi-modulo grazie alla scomposizione modulare del contesto.

4. Risultati (Results)

Il framework è stato valutato sul benchmark FVEval (Design2SVA) utilizzando il modello Qwen3.5-35B.

Correttezza Sintattica e Funzionale: ProofLoop ha raggiunto il 93,7% di correttezza sintattica e l'82,0% di correttezza funzionale, superando drasticamente il baseline (prompt diretto senza strumenti).
Scalabilità con la Complessità: Mentre le prestazioni del prompt diretto degradano all'aumentare della dimensione del design (a causa dei limiti della finestra di contesto), ProofLoop mantiene una precisione stabile grazie all'uso dell'AST e del RAG.
Analisi di Ablazione: Lo studio conferma che ogni componente è essenziale: il ciclo di verifica fornisce il contributo maggiore, seguito dagli strumenti di analisi strutturale e dalla ricerca RAG.
Confronto con lo Stato dell'Arte: Sul benchmark Design2SVA, ProofLoop ha superato significativamente modelli come GPT-4o e Gemini-1.5-Pro in termini di pass@1 e pass@5.

5. Significato e Conclusioni (Significance)

Il lavoro dimostra che il futuro della verifica automatizzata non risiede solo in modelli linguistici più grandi, ma nell'integrazione di agenti intelligenti con strumenti di verifica formale specializzati. ProofLoop colma il divario tra il linguaggio naturale (specifiche dell'ingegnere) e la logica formale (SVA), fornendo un metodo robusto e scalabile per automatizzare una delle fasi più costose e critiche del ciclo di progettazione dei semiconduttori.