Otto dimostrazioni formali verdi sono diventate cinque archiviabili quando ho verificato le asserzioni SystemVerilog
Ho osservato una dashboard formale sintetica riportare 8/8 PROVEN, per poi vedere il suo stesso audit certificarne solo 5/8 come TRUSTWORTHY. Questo ribaltamento è la premessa di Proof Firewall, la nostra dimostrazione eseguibile di governance per le asserzioni SystemVerilog (SVA) generate dall'IA, e ha cambiato i criteri che pretendo da una dimostrazione verde prima che raggiunga una revisione di sign-off per il tape-out.
Ho costruito la dashboard con proprietà "create da LLM" tramite fixture su un arbitro sintetico, una pipeline a due stadi e un attraversamento CDC perché il caso scomodo merita di essere visibile. Un'asserzione può sembrare perfettamente rispettabile in un registro delle proprietà. Un motore formale può restituire un risultato verde. Eppure l'implicazione potrebbe non aver mai dovuto svolgere alcun lavoro, o potrebbe continuare a passare anche dopo che il comportamento rilevante del progetto è stato compromesso. Avevo trattato la parola PROVEN come un punto di arrivo. Costruire questa demo mi ha costretto a considerarla come l'inizio di un riesame delle prove.
La demo di Proof Firewall non sostituisce un motore formale, non acquisisce RTL reale né invoca un LLM attivo nel suo percorso predefinito. È deliberatamente più compatta e più ispezionabile: un model checker a stati espliciti in puro Python valuta un IR sintetico del sistema di transizione, quindi un gate di governance verifica la raggiungibilità degli antecedenti, il kill delle mutazioni e il cono di influenza (COI). L'output è un motivo per archiviare un certificato di dimostrazione firmato oppure un motivo per trattenere il risultato per una revisione umana.
Sono partito con il tipo di verde sbagliato
Ricordo che la prima versione della dashboard sembrava rassicurante proprio perché era così pulita. Otto proprietà, otto badge verdi e una vista del flusso di base che faceva sembrare il lavoro completato. Il mio primo istinto è stato far spiegare meglio alla demo quel risultato pulito. Pensavo che il compito ingegneristico fosse la presentazione: portare alla luce le prove, mostrare le asserzioni, rendere la dashboard più facile da considerare affidabile. Il risultato verde era reale, ma rispondeva a una domanda più limitata rispetto a quella che un revisore deve porsi.
Poi ho sottoposto le stesse otto proprietà alle verifiche che una decisione di archiviazione richiede davvero. L'antecedente è mai diventato vero? L'asserzione solleverebbe obiezioni se una parte rilevante del progetto venisse modificata? Vincola un COI significativo? Queste domande sono meno lusinghiere di un badge verde perché chiedono cosa la dimostrazione si sia guadagnata, non semplicemente cosa il risolutore abbia restituito.
Ho dovuto abbandonare la prima impostazione della build. Una schermata che mostrava 8/8 PROVEN era una vista accurata del riferimento del flusso di base, ma era incompleta come resoconto di sign-off. Dopo l'audit del firewall, la stessa dashboard sintetica fissa presenta cinque esiti TRUSTWORTHY, un esito VACUOUS e due esiti WEAK. I restanti tre non vengono rietichettati come un successo. Vengono trattenuti insieme alle prove che spiegano il perché. L'etichetta di una dimostrazione e una decisione di archiviazione sono artefatti diversi.
Ho scelto la parola "governance" con cura. I controlli deterministici della demo rendono la decisione di archiviazione verificabile. Un autore SVA opzionale può proporre un'asserzione, ma sono il model checker e il gate delle policy a determinare il verdetto. Gli agenti consigliano, il codice decide. Cercavo di rendere il gate sufficientemente trasparente affinché il risultato negativo risultasse utile anziché semplicemente imbarazzante. Un risultato trattenuto richiede una motivazione che un ingegnere di verifica possa ispezionare, riprodurre e contestare.
ARB3 ha reso il problema impossibile da ignorare
Ho riscontrato il fallimento più evidente in ARB3, la proprietà dell'arbitro sintetico assert (g0 && g1) |-> (turn == 0). Nel flusso di base è verde. Quando ho aperto la sua forma d'onda e le prove di raggiungibilità, l'antecedente g0 && g1 risultava irraggiungibile in quell'arbitro sintetico. L'implicazione era stata dimostrata solo nel senso limitato di non essere mai stata costretta a rispondere dello stato descritto. L'antecedente non scatta mai.
Questa distinzione è facile da esprimere a parole ma difficile da tenere a mente quando una dashboard di verifica è piena di verde. Inizialmente avevo interpretato l'implicazione come un'asserzione sul comportamento dell'arbitraggio. Il risultato di raggiungibilità ha cambiato ciò che stavo osservando. Era un'asserzione la cui condizione di attivazione non si verificava mai. Definirla VACUOUS è più utile che preservare un'etichetta verde, perché indirizza il revisore verso l'assunzione o lo stimolo che ha reso vuota la dimostrazione.
Continuavo a tornare su questo pannello mentre lavoravo alle etichette delle policy. VACUOUS può sembrare un verdetto severo finché non si considera l'alternativa. Se un registro di sign-off conserva una dimostrazione senza registrare che il suo antecedente non scatta mai, la revisione ha ricevuto una conclusione priva della condizione che le dà significato. Il registro migliore è quello che rende esplicito il limite e lascia a un essere umano qualcosa di concreto su cui interrogarsi. Quel record di raggiungibilità deve stare accanto al verdetto.
Ho dovuto anche resistere alla tentazione di trattare la vacuità come un semplice avvertimento formale. Se la proprietà ha lo scopo di vincolare una condizione di arbitraggio, un comportamento di attivazione irraggiungibile costituisce una prova fondamentale del fatto che la proprietà abbia o meno esercitato il comportamento previsto. La dashboard non dovrebbe chiedere a un revisore di dedurlo da un risultato verde. Dovrebbe preservare il riscontro di raggiungibilità, escludere il risultato dal percorso di certificazione e rendere ovvia l'azione di revisione successiva.
Il contesto del settore ha reso la posta in gioco ancora più evidente per me. Lo studio del 2024 di Wilson Research Group / Siemens EDA citato nelle specifiche della demo riporta un successo al primo silicio del 14%. Non si tratta di una misurazione di Veriprajna, e questa dashboard sintetica non pretende di spiegare tale cifra. Tuttavia mi rende molto meno disposto a considerare uno stato gradevole della dashboard come una prova di per sé.
La proprietà della pipeline è sopravvissuta al guasto che mi aspettavo rilevasse
Ho incontrato il secondo fallimento durante il test di PIPE3, una proprietà di una pipeline sintetica a due stadi: assert v2 |-> (s2 == s2). Volevo un esempio conciso di un'asserzione che suonasse abbastanza ragionevole da superare una revisione superficiale. Il conseguente è una tautologia. Afferma che s2 è uguale a se stesso. Il conseguente non vincola alcunché.
Il passaggio fondamentale nella demo non è semplicemente individuare la tautologia nel testo. Il gate di governance inietta mutazioni di progetto a singolo punto rilevanti e verifica se la proprietà le elimini. Per il caso in evidenza della pipeline debole, PIPE3 registra un risultato di uccisione delle mutazioni di 0/6. La proprietà sopravvive alle varianti difettose pertinenti. Ecco perché la policy assegna WEAK anziché consentire al semplice risultato PROVEN di valere come prova per l'archiviazione. Il risultato delle mutazioni testa una sensibilità utile.
Ho imparato qualcosa di scomodo cercando di rendere questo esempio meno ovvio. Un essere umano può leggere s2 == s2 e scartarlo rapidamente. Molte debolezze non si manifesteranno in modo così evidente. Ecco perché non volevo che la demo dipendesse dalla capacità dell'operatore di individuare una stringa sospetta. L'artefatto utile è la procedura: raggiungibilità, un test di uccisione delle mutazioni pertinente, COI e una decisione di policy che ne registri la motivazione.
Sono giunto a considerare il controllo delle mutazioni come un modo rigoroso per rifiutare un'interpretazione fin troppo comoda di una dimostrazione. L'obiettivo non è fabbricare un fallimento spettacolare. È chiedersi se la proprietà noterebbe una variazione locale rilevante nel comportamento che dovrebbe vincolare. Quando non lo fa, il risultato fornisce al revisore un'indicazione operativa: questa asserzione deve essere rafforzata o instradata verso un percorso di revisione diverso prima di poter supportare il registro di sign-off.
Questo è anche il motivo per cui il benchmark della demo richiede una descrizione circoscritta. La sua esecuzione locale con python -m backend.bench ottiene un punteggio di 18/18 rispetto a un set fisso ed etichettato di asserzioni sintetiche e identifica 6 dimostrazioni che il riferimento non controllato della demo avrebbe convalidato automaticamente senza verifica. Tali cifre rappresentano un controllo di riproducibilità sulle fixture etichettate di questa demo. Non costituiscono un tasso di produzione, un'affermazione generale sulle asserzioni generate dall'IA o un confronto con strumenti formali commerciali.
Ho smesso di cercare di far apparire permissivo il gate
Dopo i primi risultati dell'audit mi sono trovato di fronte a una scelta progettuale: addolcire i verdetti trattenuti per rendere la dashboard più ottimistica, oppure lasciare che la dashboard rifiutasse di certificare ciò che non poteva difendere. Ho scelto la seconda strada perché una reale revisione di sign-off deve essere in grado di distinguere una dimostrazione completa da una limitata (bounded), un antecedente irraggiungibile da una proprietà significativa, e un controllo debole da uno che reagisce a comportamenti difettosi rilevanti. Trattenere un risultato è un esito di revisione, non un vicolo cieco.
Questa scelta si riflette nel vocabolario delle policy. TRUSTWORTHY ottiene il certificato di dimostrazione firmato. BOUNDED-PROVEN, VACUOUS, WEAK, DEAD e VIOLATED conservano motivi diversi per trattenere tale certificato o inoltrare il risultato a un livello superiore. Nella fixture CDC, ad esempio, la proprietà più forte assert (req && !ack) |-> ##1 req risulta VIOLATED e produce una concreta forma d'onda sintetica di controesempio. Illustra una classe di guasto CDC o di transazione persa. Non dice nulla sul chip di un cliente.
Non vedo tutto questo come una proposta per sostituire il motore esistente di un team di verifica. L'orientamento per la produzione è indipendente dal motore: posizionare un gate attorno a un flusso formale esistente, per poi rendere ispezionabili i relativi criteri di accettazione. Gli adattatori per motori reali e l'ingestione RTL sono rinviati in questa demo. Il perimetro dimostrato è intenzionalmente ristretto. Tale perimetro è importante perché mantiene l'affermazione proporzionata a ciò che è effettivamente in esecuzione.
Ora voglio la ricevuta accanto al verdetto
Continuo a pensare all'artefatto di cui una riunione di sign-off ha bisogno quando l'autore delle asserzioni è assistito dall'IA. Non è un punteggio di confidenza fornito dall'autore. È un record che indica quali controlli sono stati eseguiti, quale sia stato il risultato di raggiungibilità, quali mutazioni siano state eliminate, cosa contenesse il COI e perché la policy abbia concesso o negato la certificazione. La revisione necessita di prove che sia possibile riaprire.
Questo è ciò che la demo esporta in signoff_certificate.json: verdetti per singola proprietà, raggiungibilità, risultati delle mutazioni, COI, record di controesempi ove applicabile e un campo SHA-256. Ho creato il certificato come record dimostrativo affinché un revisore possa ricostruire la decisione senza dover accettare un badge verde sulla parola. Un certificato dovrebbe preservare il percorso che ha condotto al suo verdetto.
E se preferisci vederlo all'opera piuttosto che leggermi mentre lo descrivo, ecco l'intero sistema in esecuzione end-to-end.
Ho reso la demo eseguibile affinché il ribaltamento da 8/8 a 5/8 possa essere ispezionato anziché ripetuto come uno slogan. La conclusione che ne traggo è modesta ma duratura: una dimostrazione degna di archiviazione porta con sé le prove di ciò che ha vincolato, di ciò a cui è sopravvissuta e del perché ci si possa fidare di essa. Il verde rimane utile. Ha semplicemente bisogno di un record che consenta al revisore successivo di decidere se meriti di andare avanti.
