Acht grüne formale Beweise wurden zu fünf freigabefähigen, als ich die SystemVerilog-Assertions auditierte
Ich sah, wie ein synthetisches Formal-Board 8/8 PROVEN meldete, und erlebte dann, wie sein eigenes Audit lediglich 5/8 als TRUSTWORTHY zertifizierte. Dieser Umschwung ist der Ausgangspunkt von Proof Firewall, unserer ausführbaren Demonstration von Governance für KI-generierte SystemVerilog-Assertions (SVA), und er hat den Maßstab verändert, den ein grüner Beweis für mich erfüllen muss, bevor er ein Tape-Out-Sign-Off-Review erreicht.
Ich habe das Board mit fixture-erstellten, „LLM-generierten“ Properties auf einem synthetischen Arbiter, einer zweistufigen Pipeline und einem CDC-Crossing aufgebaut, weil der unbequeme Fall sichtbar sein muss. Eine Assertion kann in einem Property-Ledger vollkommen solide wirken. Eine Formal-Engine kann ein grünes Ergebnis liefern. Dennoch musste die Implikation möglicherweise nie tatsächliche Arbeit leisten, oder sie besteht weiterhin, nachdem das relevante Designverhalten zerstört wurde. Zuvor hatte ich das Wort PROVEN als Zielpunkt betrachtet. Der Bau dieser Demo zwang mich dazu, es als Beginn einer Evidenzprüfung zu behandeln.
Die Proof-Firewall-Demo ersetzt keine Formal-Engine, liest kein echtes RTL ein und ruft im Standardpfad kein Live-LLM auf. Sie ist bewusst kleiner und besser überprüfbar: Ein Explicit-State-Model-Checker in reinem Python wertet eine synthetische Transitionssystem-IR aus; anschließend prüft ein Governance-Gate die Erreichbarkeit des Antezedens, Mutation-Kills und den Cone of Influence (COI). Die Ausgabe ist entweder ein Grund, ein signiertes Demonstrationszertifikat abzulegen, oder ein Grund, das Ergebnis für eine menschliche Überprüfung zurückzuhalten.
Ich begann mit der falschen Art von Grün
Ich erinnere mich daran, dass sich die erste Version des Boards gerade deshalb so beruhigend anfühlte, weil sie so sauber war. Acht Properties, acht grüne Badges und eine Bare-Flow-Ansicht, die die Arbeit abgeschlossen aussehen ließ. Mein erster Instinkt war, die Demo so zu gestalten, dass sie dieses saubere Ergebnis besser erklärt. Ich dachte, die Engineering-Aufgabe läge in der Präsentation: die Beweise hervorheben, die Assertions zeigen, das Dashboard vertrauenswürdiger machen. Das grüne Ergebnis war real, aber es beantwortete eine weitaus begrenztere Frage als jene, die ein Prüfer stellen muss.
Dann unterzog ich dieselben acht Properties den Prüfungen, die ein Sign-Off-Gespräch tatsächlich erfordert. Wurde das Antezedens überhaupt jemals wahr? Würde die Assertion Einspruch erheben, wenn ein relevanter Teil des Designs geändert würde? Schränkt sie einen aussagekräftigen COI ein? Diese Fragen sind weniger schmeichelhaft als ein grünes Badge, weil sie danach fragen, was der Beweis geleistet hat, und nicht bloß, was der Solver zurückgegeben hat.
Ich musste die ursprüngliche Konzeption des Setups verwerfen. Ein Bildschirm, der 8/8 PROVEN zeigte, war zwar ein akkurates Bild der Bare-Flow-Baseline, aber unvollständig für einen belastbaren Sign-Off. Nach dem Firewall-Audit weist dasselbe feste synthetische Board fünf TRUSTWORTHY-Ergebnisse, ein VACUOUS-Ergebnis und zwei WEAK-Ergebnisse auf. Die verbleibenden drei werden nicht als Erfolg umdeklariert. Sie werden zusammen mit den Nachweisen zurückgehalten, die erklären, warum. Ein Beweis-Label und eine Freigabeentscheidung sind unterschiedliche Artefakte.
Ich habe das Wort „Governance“ hier mit Bedacht gewählt. Die deterministischen Prüfungen der Demo machen die Sign-Off-Entscheidung nachvollziehbar. Ein optionaler SVA-Autor mag eine Assertion vorschlagen, aber der Model-Checker und das Policy-Gate bestimmen das Urteil. Agenten beraten, Code entscheidet. Ich wollte das Gate so transparent gestalten, dass ein negatives Ergebnis nützlich ist, statt bloß peinlich zu wirken. Ein zurückgehaltenes Ergebnis braucht eine Begründung, die ein Verifikationsingenieur untersuchen, reproduzieren und anfechten kann.
ARB3 machte das Problem unübersehbar
Den deutlichsten Fehler fand ich in ARB3, der synthetischen Arbiter-Property assert (g0 && g1) |-> (turn == 0). Im Bare Flow ist sie grün. Als ich ihr Signalverlaufsdiagramm und den Erreichbarkeitsnachweis öffnete, war das Antezedens g0 && g1 in diesem synthetischen Arbiter unerreichbar. Die Implikation war nur in dem engen Sinne bewiesen, dass sie nie für den Zustand einstehen musste, den sie beschrieb. Das Antezedens feuert nie.
Diese Unterscheidung lässt sich leicht aussprechen, gerät aber schnell aus dem Blick, wenn ein Verifikations-Dashboard voller Grün ist. Zunächst verstand ich die Implikation als Aussage über das Arbitrierungsverhalten. Das Erreichbarkeitsergebnis veränderte meine Perspektive: Es handelte sich um eine Aussage, deren auslösende Bedingung niemals eintrat. Dies als VACUOUS zu bezeichnen, ist nützlicher, als ein grünes Label beizubehalten, da es den Prüfer direkt auf die Annahme oder den Stimulus hinweist, der den Beweis inhaltsleer gemacht hat.
Ich bin bei der Arbeit an den Policy-Labels immer wieder zu diesem Panel zurückgekehrt. VACUOUS mag wie ein hartes Urteil klingen, bis man die Alternative bedenkt. Wenn ein Sign-Off-Protokoll einen Beweis festhält, ohne zu dokumentieren, dass sein Antezedens nie feuert, erhält das Review eine Schlussfolgerung ohne die Bedingung, die ihr Bedeutung verleiht. Der bessere Nachweis ist jener, der die Einschränkung explizit macht und einer Person konkrete Anhaltspunkte zur Überprüfung liefert. Dieser Erreichbarkeitsnachweis gehört direkt neben das Urteil.
Ich musste mich auch dagegen wehren, Vakuität als kosmetische Warnung abzutun. Wenn die Property eine Arbitrierungsbedingung einschränken soll, ist unerreichbares Trigger-Verhalten ein zentraler Beleg dafür, ob die Property das beabsichtigte Verhalten überhaupt geprüft hat. Das Dashboard sollte von einem Prüfer nicht verlangen, dies aus einem grünen Ergebnis abzuleiten. Es sollte den Erreichbarkeitsbefund festhalten, das Ergebnis aus dem Zertifikatspfad leiten und den nächsten Prüfungsschritt offensichtlich machen.
Der Branchenkontext hat mir die Dringlichkeit verdeutlicht. Die in der Demo-Spezifikation zitierte Studie der Wilson Research Group / Siemens EDA aus dem Jahr 2024 berichtet von 14 % First-Silicon-Erfolg. Das ist keine Messung von Veriprajna, und dieses synthetische Board erhebt nicht den Anspruch, diese Zahl zu erklären. Es führt jedoch dazu, dass ich einen erfreulichen Dashboard-Zustand noch weniger als eigenständigen Beweis akzeptiere.
Die Pipeline-Property überstand genau den Fehler, den sie eigentlich abfangen sollte
Auf den zweiten Fehler stieß ich beim Testen von PIPE3, einer synthetischen zweistufigen Pipeline-Property: assert v2 |-> (s2 == s2). Ich wollte ein prägnantes Beispiel für eine Assertion, die plausibel genug klingt, um ein oberflächliches Review zu passieren. Die Konsequenz ist eine Tautologie. Sie besagt, dass s2 sich selbst gleicht. Die Konsequenz schränkt rein gar nichts ein.
Der entscheidende Schritt in der Demo besteht nicht nur darin, die Tautologie im Text zu erkennen. Das Governance-Gate injiziert relevante Einzelpunkt-Designmutationen und prüft, ob die Property diese abtötet. Für den vorgestellten schwachen Pipeline-Fall verzeichnet PIPE3 ein 0/6-Mutation-Kill-Ergebnis. Die Property übersteht die relevanten fehlerhaften Varianten. Aus diesem Grund weist die Policy WEAK zu, anstatt das reine Ergebnis PROVEN als Sign-Off-Nachweis stehenzulassen. Das Mutationsergebnis testet die tatsächliche Sensitivität.
Ich habe eine unbequeme Lektion gelernt, als ich versuchte, dieses Beispiel weniger offensichtlich zu gestalten. Ein Mensch kann s2 == s2 lesen und sofort abtun. Viele Schwachstellen kündigen sich jedoch nicht so deutlich an. Deshalb wollte ich nicht, dass die Demo davon abhängt, dass der Prüfer eine verdächtige Zeichenkette bemerkt. Das nützliche Artefakt ist das Verfahren: Erreichbarkeit, ein relevanter Mutation-Kill-Test, COI und eine Policy-Entscheidung, die ihre Begründung protokolliert.
Ich begann, die Mutationsprüfung als disziplinierte Methode zu begreifen, eine allzu bequeme Interpretation eines Beweises abzulehnen. Das Ziel ist nicht, ein dramatisches Scheitern künstlich herbeizuführen. Es geht darum zu fragen, ob die Property eine relevante lokale Änderung des Verhaltens bemerken würde, das sie eigentlich einschränken soll. Wenn sie das nicht tut, liefert das Ergebnis dem Prüfer eine handlungsrelevante Erkenntnis: Diese Assertion muss verstärkt werden oder einen anderen Prüfpfad durchlaufen, bevor sie das Sign-Off-Protokoll stützen kann.
Aus diesem Grund bedarf auch der Benchmark der Demo einer präzisen Eingrenzung. Sein lokaler python -m backend.bench-Lauf erzielt 18/18 gegenüber einem fest annotierten synthetischen Assertion-Set und identifiziert 6 Beweise, die die ungeprüfte Baseline der Demo einfach durchgewunken hätte. Diese Zahlen sind ein Reproduzierbarkeitsabgleich für die annotierten Fixtures dieser Demo. Sie stellen weder eine Produktionsrate dar, noch eine allgemeine Aussage über KI-generierte Assertions oder einen Vergleich mit kommerziellen Formal-Tools.
Ich hörte auf, das Gate permissiv wirken zu lassen
Nach den ersten Audit-Ergebnissen stand ich vor einer Design-Entscheidung: die zurückbehaltenden Urteile abmildern, damit das Board optimistischer wirkt, oder das Board Zertifizierungen verweigern lassen, die es nicht verteidigen kann. Ich entschied mich für Letzteres, da ein echtes Sign-Off-Review unterscheiden können muss: zwischen einem vollständigen und einem beschränkten (bounded) Beweis, zwischen einem unerreichbaren Antezedens und einer aussagekräftigen Property sowie zwischen einer schwachen Prüfung und einer solchen, die auf relevantes fehlerhaftes Verhalten reagiert. Das Zurückhalten ist ein Review-Ergebnis, keine Sackgasse.
Diese Entscheidung spiegelt sich im Vokabular der Policy wider. TRUSTWORTHY erhält das signierte Demonstrationszertifikat. BOUNDED-PROVEN, VACUOUS, WEAK, DEAD und VIOLATED halten unterschiedliche Gründe fest, um dieses Zertifikat zu verweigern oder das Ergebnis zu eskalieren. In der CDC-Fixture beispielsweise wird die stärkere Property assert (req && !ack) |-> ##1 req als VIOLATED eingestuft und erzeugt ein konkretes synthetisches Gegenbeispiel-Signalverlaufsdiagramm. Sie veranschaulicht eine Lost-Transaction- oder CDC-Fehlerklasse. Sie trifft keinerlei Aussage über den Chip eines Kunden.
Ich betrachte dies nicht als Plädoyer dafür, die bestehende Engine eines Verifikationsteams zu ersetzen. Die Produktionsausrichtung ist Engine-agnostisch: Man legt ein Gate um einen bestehenden Formal-Workflow und macht dessen Abnahmekriterien überprüfbar. Adapter für reale Engines und der RTL-Import sind in dieser Demo zurückgestellt. Die demonstrierte Grenze ist bewusst eng gesteckt. Diese Abgrenzung ist wichtig, weil sie die Aussagekraft proportional zu dem hält, was tatsächlich ausgeführt wird.
Ich will den Beleg jetzt direkt neben dem Urteil sehen
Ich denke immer wieder an das Artefakt, das ein Sign-Off-Meeting benötigt, wenn der Assertion-Autor durch KI unterstützt wird. Es ist kein Konfidenzwert des Autors. Es ist ein Protokoll, das darlegt, welche Prüfungen liefen, wie das Erreichbarkeitsergebnis ausfiel, welche Mutationen abgetötet wurden, was der COI enthielt und warum die Policy die Zertifizierung erteilte oder verweigerte. Das Review braucht Evidenz, die es jederzeit wieder aufrollen kann.
Genau das exportiert die Demo in signoff_certificate.json: Urteile pro Property, Erreichbarkeit, Mutationsergebnisse, COI, Gegenbeispiel-Protokolle, sofern zutreffend, und ein SHA-256-Feld. Ich habe das Zertifikat als Demonstrationsnachweis aufgebaut, damit ein Prüfer die Entscheidung rekonstruieren kann, anstatt ein grünes Badge blind zu glauben. Ein Zertifikat sollte den Weg zu seinem Urteil bewahren.
Und falls Sie es lieber sehen möchten, statt nur meine Beschreibung zu lesen: Hier läuft das Ganze von Anfang bis Ende durch.
Ich habe die Demo ausführbar gemacht, damit der Umschwung von 8/8 auf 5/8 untersucht werden kann, anstatt ihn als Slogan zu wiederholen. Die Erkenntnis, die ich daraus mitnehme, ist bescheiden, aber beständig: Ein belegbarer Beweis liefert den Nachweis darüber, was er eingeschränkt hat, was er überstanden hat und warum man sich darauf verlassen kann. Grün bleibt nützlich. Es braucht lediglich ein Protokoll, das dem nächsten Prüfer die Entscheidung ermöglicht, ob es verdient, weitergereicht zu werden.
