Autoformalizing Memory Specifications with Agents

1. Enunciato del Problema

La fase di Design Verification (DV) nella progettazione di chip semiconduttori rappresenta un collo di bottiglia significativo, assorbendo oltre il 50% del ciclo di vita della progettazione. La sfida principale risiede nella traduzione delle specifiche non strutturate in linguaggio naturale (ad esempio, gli standard JEDEC per i chip di memoria) in modelli formali ed eseguibili richiesti per la verifica.

Gli approcci AI attuali si concentrano tipicamente sulla generazione di SystemVerilog Assertions (SVAs) isolati. Tuttavia, questo approccio presenta limitazioni significative:

• Incompletezza: Gli SVA verificano proprietà specifiche ma non generano modelli comportamentali completi, generatori di stimoli o metriche di copertura funzionale.
• Ambiguità: Le specifiche in linguaggio naturale contengono spesso ambiguità che portano i LLM a generare asserzioni sintatticamente non valide o non allineate al protocollo.
• Complessità: Gli standard di memoria moderni (DDR5, HBM3, GDDR7) coinvolgono vincoli temporali intricati, interazioni di comandi complesse e strutture gerarchiche difficili da catturare con una semplice generazione da prompt a codice.

2. Metodologia

Gli autori propongono un Framework di Autoformalizzazione Agente che converte le specifiche di memoria in linguaggio naturale in una rappresentazione intermedia strutturata ed eseguibile chiamata DRAMPyML, anziché generare direttamente SVAs.

2.1 La Rappresentazione Intermedia: DRAMPyML

Invece di saltare direttamente alle asserzioni, il sistema mira a DRAMPyML, un linguaggio di modellazione basato su Python costruito su Reti di Petri Temporizzate.

• Struttura: Modella i dispositivi di memoria come una tupla di posti (banche, ranghi), transizioni (comandi come ACT, RD, WR) e archi (regolari, inibitori, reset e temporizzati).
• Vantaggi: Questa rappresentazione è eseguibile, consentendo la generazione di tracce di comandi, stimoli e controlli temporali. Funge da fonte unificata da cui possono essere derivati a valle SVAs, testbench e modelli di copertura.
• Definizioni Formali: Il paper definisce matematicamente le Reti di Petri DRAM e introduce il concetto di Equivalenza delle Tracce. Ipotizza (e valida empiricamente) la Congettura 3.4: verificare l'equivalenza delle tracce per configurazioni piccole (ad esempio, 1 o 2 banche) con lunghezze di traccia brevi ($k=4$) è sufficiente a dimostrare l'equivalenza per l'intero dispositivo complesso, a causa delle proprietà di simmetria.

2.2 L'Agente di Autoformalizzazione

Il sistema impiega un Flusso di Lavoro Agente iterativo (Figura 2 nel paper) anziché un approccio di generazione singola:

1. Input: L'agente riceve specifiche PDF JEDEC, datasheet dei vendor e la libreria DRAMPyML.
2. Ciclo Iterativo: L'agente utilizza strumenti (server MCP, API LLM) per:
   • Leggere sezioni specifiche della specifica.
   • Scrivere o modificare codice Python per costruire il grafo della Rete di Petri.
   • Auto-Validazione: Eseguire test di validazione interni (controllando deadlock, nodi orfani e generando tracce di comandi per incrociarle con la specifica).
3. Raffinamento: Sulla base del feedback di validazione, l'agente raffina iterativamente il modello fino a soddisfare la coerenza strutturale e la correttezza temporale.
4. Strategie di Prompting: Lo studio confronta il prompting One-Shot (singolo prompt con convenzioni esplicite) rispetto all'approccio Agente (interazione iterativa con l'ambiente e gli strumenti).

3. Contributi Chiave

1. DRAMBench: Il rilascio del primo benchmark open-source per l'autoformalizzazione hardware, contenente formalizzazioni DRAMPyML ground-truth per 13 standard JEDEC (che coprono DDR2-5, LPDDR2-5, GDDR5-7 e HBM2-3).
2. Framework Agente: Dimostrazione che un agente iterativo che utilizza la validazione potenziata da strumenti supera significativamente la generazione one-shot, in particolare per specifiche complesse.
3. Validazione Teorica ed Empirica:
   • Definizione formale delle Reti di Petri DRAM e dell'equivalenza delle tracce.
   • Prova empirica che il controllo di tracce brevi ($k \le 4$) su configurazioni minime (1-2 banche) è sufficiente per rilevare bug semantici nei modelli generati, aggirando il problema dell'esplosione dello spazio degli stati.
4. Risultati del Benchmarking: Una valutazione completa dei modelli all'avanguardia (Sonnet 4.5, GPT-5.2, DeepSeek-v3p2) che mostra i compromessi tra costo in token e prestazioni.

4. Risultati Sperimentali

Gli autori hanno valutato i modelli sul dataset DRAMBench utilizzando due metriche:

• Indice di Jaccard: Misura la sovrapposizione delle tracce di comandi legali tra il modello generato e la ground truth.
• Recall dei Vincoli Temporali: Misura la frazione di vincoli temporali ground truth correttamente recuperati.

Risultati Chiave:

• Agente vs One-Shot: L'approccio agente ha raggiunto costantemente prestazioni di picco più elevate, specialmente per standard complessi (ad esempio, DDR5, HBM3) e quando non venivano forniti esempi. La generazione one-shot ha faticato con il formato di output non familiare senza forti prior.
• Impatto degli Esempi: Fornire esempi "scelti con cura" (ad esempio, utilizzare DDR3 per aiutare a generare DDR4) ha aumentato significativamente le prestazioni per entrambi i metodi, permettendo talvolta ai modelli one-shot di superare gli agenti su compiti più semplici.
• Prestazioni dei Modelli:
  • DeepSeek-v3p2 (open-weight) ha performato in modo competitivo rispetto ai modelli closed-source (Sonnet 4.5, GPT-5.2), superandoli spesso nell'ambiente agente.
  • Sonnet 4.5 ha raggiunto la massima perfezione strutturale per standard come HBM2 e DDR2-4 quando forniti con esempi.
• Modalità di Fallimento: L'analisi di fallimenti complessi (ad esempio, DDR5) ha rivelato che gli agenti faticano con:
  • La selezione di primitive corrette (ad esempio, comandi precharge errati).
  • La modellazione della gerarchia di memoria (ad esempio, gruppi di banche).
  • L'imposizione di vincoli temporali al corretto livello di astrazione (disallineamenti di coordinate che causano l'inattivazione degli archi temporali).
• Efficienza dei Token: Sebbene gli agenti raggiungano una maggiore accuratezza, consumano più token. Tuttavia, per specifiche complesse, la curva "token vs. prestazioni" favorisce l'agente, poiché i modelli one-shot non riescono a convergere su strutture corrette indipendentemente dal numero di token.

5. Significato

Questo lavoro rappresenta un cambiamento di paradigma nella verifica hardware:

• Dalle Asserzioni ai Modelli: Si sposta oltre la generazione di asserzioni isolate per creare modelli comportamentali strutturati ed eseguibili. Ciò abilita uno "shift-left" nella verifica, consentendo il rilevamento precoce di difetti di progettazione e la generazione automatica di collateral diversificati (stimoli, copertura, SVAs).
• Scalabilità: Sfruttando la rappresentazione intermedia DRAMPyML e il controllo di equivalenza delle tracce, il metodo offre un percorso scalabile per verificare dispositivi di memoria moderni e altamente paralleli che erano precedentemente troppo complessi per l'autoformalizzazione automatizzata.
• Scienza Aperta: Il rilascio di DRAMBench fornisce un benchmark standardizzato e di livello professionale che mancava precedentemente nella letteratura AI per l'Hardware, permettendo alla comunità di tracciare i progressi nell'autoformalizzazione hardware.

In conclusione, il paper dimostra che i flussi di lavoro agenti combinati con rappresentazioni intermedie strutturate (Reti di Petri) sono il percorso più percorribile verso l'automazione della verifica di standard semiconduttori complessi, superando i limiti degli attuali approcci LLM diretti alle asserzioni.