Acht groene formele bewijzen werden vijf indienbare bewijzen toen ik de SystemVerilog-asserties auditte
Ik zag een synthetisch formeel dashboard 8/8 PROVEN rapporteren, en zag vervolgens hoe de eigen audit slechts 5/8 als TRUSTWORTHY certificeerde. Die omkering is het uitgangspunt van Proof Firewall, onze uitvoerbare demonstratie van governance voor door AI gegenereerde SystemVerilog-asserties (SVA), en het veranderde de norm waaraan een groen bewijs volgens mij moet voldoen voordat het een tape-out sign-off review bereikt.
Ik bouwde het dashboard met door fixtures opgestelde "door LLM geschreven" eigenschappen op een synthetische arbiter, een tweetraps pipeline en een CDC-kruising, omdat het ongemakkelijke scenario zichtbaar moet zijn. Een assertie kan er in een property ledger volkomen respectabel uitzien. Een formele engine kan een groen resultaat opleveren. Toch hoefde de implicatie wellicht nooit enig werk te verrichten, of blijft deze slagen nadat het relevante ontwerpgedrag is gebroken. Ik had het woord PROVEN behandeld als een eindbestemming. Het bouwen van deze demo dwong me om het te beschouwen als het begin van een evaluatie van het bewijsmateriaal.
De Proof Firewall-demo vervangt geen formele engine, leest geen echte RTL in en roept in zijn standaardpad geen live LLM aan. Hij is met opzet kleiner en beter inspecteerbaar: een explicit-state model checker in puur Python evalueert een synthetische transitiesysteem-IR, waarna een governance-poort de antecedent-bereikbaarheid, mutatie-kills en cone of influence (COI) controleert. De uitvoer is ofwel een reden om een ondertekend demonstratiecertificaat in te dienen, ofwel een reden om het resultaat aan te houden voor menselijke beoordeling.
Ik begon met het verkeerde soort groen
Ik herinner me dat de eerste versie van het dashboard geruststellend aanvoelde, juist omdat hij zo clean was. Acht eigenschappen, acht groene badges en een bare-flow-weergave die het werk afgerond deed lijken. Mijn eerste instinct was om de demo dat cleane resultaat beter te laten uitleggen. Ik dacht dat de technische taak presentatie was: de bewijzen naar boven halen, de asserties tonen, het dashboard gemakkelijker te vertrouwen maken. Het groene resultaat was reëel, maar het beantwoordde een beperktere vraag dan degene die een reviewer moet stellen.
Vervolgens onderwierp ik diezelfde acht eigenschappen aan de controles die een indieningsgesprek daadwerkelijk vereist. Werd het antecedent ooit waar? Zou de assertie bezwaar maken als een relevant onderdeel van het ontwerp werd gewijzigd? Legt het beperkingen op aan een betekenisvolle COI? Die vragen zijn minder vleiend dan een groene badge, omdat ze vragen wat het bewijs heeft verdiend, en niet slechts wat de solver heeft geretourneerd.
Ik moest de eerste opzet van de build loslaten. Een scherm dat 8/8 PROVEN toonde was een nauwkeurige weergave van de bare-flow-baseline, maar het was onvolledig als sign-off-verhaal. Na de firewall-audit heeft hetzelfde vaste synthetische dashboard vijf TRUSTWORTHY-resultaten, één VACUOUS-resultaat en twee WEAK-resultaten. De overige drie worden niet omgedoopt tot succes. Ze worden aangehouden met het bewijsmateriaal dat uitlegt waarom. Een bewijslabel en een indieningsbeslissing zijn verschillende artefacten.
Ik heb het woord "governance" hier zorgvuldig gekozen. De deterministische controles van de demo maken de indieningsbeslissing toetsbaar. Een optionele SVA-auteur kan een assertie voorstellen, maar de model checker en de beleidspoort bepalen het oordeel. Agents adviseren, code beslist. Ik probeerde de poort transparant genoeg te maken zodat het negatieve resultaat nuttig zou zijn in plaats van louter beschamend. Een ingehouden resultaat heeft een reden nodig die een verificatie-engineer kan inspecteren, reproduceren en aanvechten.
ARB3 maakte het probleem onmogelijk te negeren
Ik vond het duidelijkste falen in ARB3, de synthetische arbitereigenschap assert (g0 && g1) |-> (turn == 0). In de bare flow is deze groen. Toen ik de golfvorm en het bereikbaarheidsbewijs opende, bleek het antecedent g0 && g1 onbereikbaar te zijn in die synthetische arbiter. De implicatie was uitsluitend bewezen in de enge zin dat ze nooit ter verantwoording werd geroepen voor de toestand die ze beschreef. Het antecedent vuurt nooit.
Dat onderscheid is gemakkelijk uit te spreken en moeilijk scherp voor ogen te houden wanneer een verificatiedashboard vol groen staat. Aanvankelijk las ik de implicatie als een claim over arbitergedrag. Het bereikbaarheidsresultaat veranderde waar ik naar keek. Het was een claim waarvan de triggerende voorwaarde nooit optrad. Dat VACUOUS noemen is nuttiger dan een groen label behouden, omdat het de reviewer wijst op de aanname of stimulus die het bewijs inhoudsloos maakte.
Ik bleef terugkeren naar dit paneel tijdens het werken aan de beleidslabels. VACUOUS kan klinken als een hard resultaat totdat het alternatief in overweging wordt genomen. Als een sign-off-dossier een bewijs behoudt zonder vast te leggen dat het antecedent nooit vuurt, heeft de beoordeling een conclusie ontvangen zonder de voorwaarde die er betekenis aan geeft. Het betere dossier is het dossier dat de beperking expliciet maakt en een mens iets concreets biedt om te bevragen. Dat bereikbaarheidsdossier hoort naast het oordeel.
Ik moest ook de neiging weerstaan om vacuïteit te behandelen als een cosmetische waarschuwing. Als de eigenschap bedoeld is om een arbitragevoorwaarde te beperken, is onbereikbaar triggergedrag cruciaal bewijsmateriaal over de vraag of de eigenschap het beoogde gedrag daadwerkelijk heeft getoetst. Het dashboard moet van een reviewer niet vragen dat af te leiden uit een groen resultaat. Het moet de bereikbaarheidsbevinding bewaren, het resultaat wegleiden uit het certificaatpad en de volgende beoordelingsactie voor de hand liggend maken.
De sectorcontext maakte de inzet voor mij nog scherper. Het onderzoek van Wilson Research Group / Siemens EDA uit 2024 dat in de demospecificatie wordt geciteerd, meldt 14% succes bij first-silicon. Dat is geen meting van Veriprajna, en dit synthetische dashboard beweert dat cijfer niet te verklaren. Het zorgt er wel voor dat ik minder bereid ben om een prettige dashboardstatus op zichzelf als bewijs te beschouwen.
De pipeline-eigenschap overleefde de fout die hij geacht werd te vangen
Ik stuitte op het tweede falen tijdens het testen van PIPE3, een synthetische tweetraps pipeline-eigenschap: assert v2 |-> (s2 == s2). Ik wilde een beknopt voorbeeld van een assertie die zinnig genoeg leest om door een oppervlakkige beoordeling te glippen. Het consequent is een tautologie. Het stelt dat s2 gelijk is aan zichzelf. Het consequent beperkt niets.
De belangrijke stap in de demo is niet louter het opmerken van de tautologie in tekst. De governance-poort injecteert relevante single-point-ontwerpmutaties en toetst of de eigenschap deze killt. Voor de uitgelichte zwakke pipeline-casus PIPE3 noteert een 0/6 mutatie-kill-resultaat. De eigenschap overleeft de relevante defecte varianten. Daarom kent het beleid WEAK toe, in plaats van het kale PROVEN-resultaat te laten gelden als indieningsbewijs. Het mutatieresultaat test nuttige gevoeligheid.
Ik leerde iets ongemakkelijks toen ik probeerde dit voorbeeld minder voor de hand liggend te maken. Een mens kan s2 == s2 lezen en het snel terzijde schuiven. Veel zwaktes zullen zich niet zo openlijk aankondigen. Daarom wilde ik niet dat de demo afhankelijk zou zijn van een operator die een verdachte string opmerkt. Het nuttige artefact is de procedure: bereikbaarheid, een relevante mutatie-killtest, COI en een beleidsbeslissing die de reden vastlegt.
Ik ging de mutatiecontrole zien als een gedisciplineerde manier om een al te gemakkelijke lezing van een bewijs te weigeren. Het doel is niet om een dramatische mislukking te creëren. Het is om te vragen of de eigenschap een relevante lokale verandering zou opmerken in het gedrag dat zij geacht wordt te beperken. Wanneer dat niet het geval is, vertelt het resultaat een reviewer iets bruikbaars: deze assertie moet worden versterkt of via een ander beoordelingstraject lopen voordat zij het sign-off-dossier kan ondersteunen.
Dit is ook de reden waarom de benchmark van de demo een nauwkeurige afbakening vereist. De lokale uitvoering van python -m backend.bench scoort 18/18 op een vaste, gelabelde synthetische assertieset en identificeert 6 bewijzen die de eigen ongegated baseline van de demo klakkeloos zou hebben goedgekeurd. Die cijfers zijn een reproduceerbaarheidscontrole op de gelabelde fixtures van deze demo. Ze vormen geen productiesnelheid, geen claim over door AI geschreven asserties in het algemeen, en geen vergelijking met commerciële formele tools.
Ik stopte met proberen de poort coulant te laten lijken
Ik stond voor een ontwerpkeuze na de eerste auditresultaten: de ingehouden oordelen afzwakken zodat het dashboard optimistischer aanvoelde, of het dashboard laten weigeren te certificeren wat het niet kon verdedigen. Ik koos voor het laatste omdat een echte sign-off review het vermogen nodig heeft om een volledig bewijs te onderscheiden van een begrensd bewijs, een onbereikbaar antecedent van een betekenisvolle eigenschap, en een zwakke controle van een controle die reageert op relevant defect gedrag. Inhouden is een beoordelingsuitkomst, geen doodlopende weg.
Die keuze komt tot uiting in het beleidsvocabulair. TRUSTWORTHY verdient het ondertekende demonstratiecertificaat. BOUNDED-PROVEN, VACUOUS, WEAK, DEAD en VIOLATED bewaren verschillende redenen om dat certificaat in te houden of het resultaat te escaleren. In de CDC-fixture is de sterkere eigenschap assert (req && !ack) |-> ##1 req bijvoorbeeld VIOLATED en levert een concrete synthetische tegenvoorbeeldgolfvorm op. Het illustreert een transactieverlies- of CDC-foutklasse. Het zegt niets over een chip van een klant.
Ik zie dit niet als een pleidooi om de bestaande engine van een verificatieteam te vervangen. De productierichting is engine-agnostisch: plaats een poort rond een bestaande formele workflow en maak vervolgens de acceptatiecriteria inspecteerbaar. Adapters voor echte engines en RTL-ingest zijn in deze demo uitgesteld. De gedemonstreerde afbakening is met opzet smal. Die afbakening is belangrijk omdat het de claim evenredig houdt aan wat er daadwerkelijk draait.
Ik wil nu het bewijsbonnetje naast het oordeel
Ik blijf nadenken over het artefact dat een sign-off-bijeenkomst nodig heeft wanneer de assertie-auteur wordt ondersteund door AI. Het is geen betrouwbaarheidsscore van de auteur. Het is een dossier dat vermeldt welke controles zijn uitgevoerd, wat het bereikbaarheidsresultaat was, welke mutaties werden gekilld, wat de COI bevatte en waarom het beleid certificering toestond of inhield. De review heeft bewijsmateriaal nodig dat opnieuw kan worden geopend.
Dat is wat de demo exporteert in signoff_certificate.json: oordelen per eigenschap, bereikbaarheid, mutatieresultaten, COI, tegenvoorbeelddossiers waar van toepassing en een SHA-256-veld. Ik heb het certificaat gebouwd als een demonstratiedossier omdat een reviewer de beslissing moet kunnen reconstrueren zonder een groene badge op goed vertrouwen te accepteren. Een certificaat moet het pad naar zijn oordeel bewaren.
En als je het liever ziet dan mijn beschrijving ervan leest: hier draait het geheel van begin tot eind.
Ik heb de demo uitvoerbaar gemaakt zodat de omkering van 8/8 naar 5/8 kan worden geïnspecteerd in plaats van herhaald als een slogan. Het inzicht dat ik eraan overhoud is bescheiden maar duurzaam: een bewijs dat het waard is om te worden ingediend, draagt het bewijsmateriaal met zich mee van wat het heeft begrensd, wat het heeft overleefd en waarom iemand erop mag vertrouwen. Groen blijft nuttig. Er is simpelweg een dossier voor nodig waarmee de volgende reviewer kan beslissen of het verdient om verder te gaan.
