當我審計了 SystemVerilog 斷言後，八個綠色形式化證明縮減為五個可歸檔證明
我親眼看著一個合成形式化看板回報 8/8 PROVEN，隨後看著它自身的審計僅證明 5/8 為 TRUSTWORTHY。這項逆轉正是 Proof Firewall 的前提——這是我們針對 AI 生成的 SystemVerilog 斷言（SVA）治理所構建的可運行示範系統，它改變了我希望綠色證明在進入流片簽核（tape-out sign-off）審查前所必須達到的標準。
我在合成仲裁器（arbiter）、兩級管線（two-stage pipeline）以及跨時鐘域（CDC）電路上，使用治具編寫的「LLM 編寫」屬性構建了該看板，因為令人不安的案例理應被看見。斷言在屬性總帳中可能看起來完全合規；形式化引擎也可能傳回綠色結果。然而，該蘊涵式（implication）可能從未真正發揮過作用，或者在相關設計行為遭到破壞後依然持續通過。我過去一直將 PROVEN 這個詞視為終點。構建這個示範系統迫使我將其視為證據審查的起點。
這套 Proof Firewall 示範系統 在其預設路徑中並不會取代形式化引擎、讀取真實 RTL，也不會呼叫即時運行的 LLM。它特意被設計得更小巧、更具可檢查性：一個純 Python 顯式狀態模型檢查器（explicit-state model checker）負責評估合成轉移系統中間表示（IR），隨後治理閘門會檢查前件可達性（antecedent reachability）、突變擊殺（mutation kills）以及影響錐（cone of influence, COI）。其輸出要麼是歸檔已簽署示範證書的理由，要麼是扣留該結果以待人工審查的理由。
我一開始追求了錯誤的綠色
我至今仍記得該看板的第一個版本令人倍感安心，恰恰因為它太乾淨了。八個屬性、八個綠色徽章，以及一個讓工作看似已經完成的裸流程（bare-flow）視圖。我早期的直覺是讓示範系統更好地解釋那個乾淨的結果。我以為工程任務在於呈現：展示證明、呈現斷言、讓儀表板更容易被信任。 那個綠色結果是真實的，但它所回答的問題，遠小於審查人員真正需要提出的問題。
隨後，我讓相同的八個屬性通過簽核歸檔對話中真正會涉及的各項檢查。前件是否曾經為真？如果設計的相關部分被改動，斷言是否會提出異議？它是否約束了有意義的 COI？這些問題比綠色徽章更不近人情，因為它們詢問的是證明真正贏得了什麼，而不僅僅是求解器傳回了什麼。
我不得不放棄構建初期的第一種構想。顯示 8/8 PROVEN 的畫面固然是裸流程基準線的精確視圖，但作為簽核故事卻是不完整的。在經過防火牆審計後，同一個固定的合成看板得出了五個 TRUSTWORTHY 結果、一個 VACUOUS 結果，以及兩個 WEAK 結果。其餘三個結果並未被重新貼上成功的標籤，而是連同解釋其原因的證據一起被扣留。 證明標籤與歸檔決策是截然不同的產物。
我在這裡審慎選擇了「治理」這個詞。示範系統的確定性檢查使歸檔決策變得可供審查。可選的 SVA 編寫者可以提出斷言，但由模型檢查器與策略閘門決定最終判決。 代理提供建議，程式碼做出決策。 我試圖讓閘門足夠清晰易懂，使否定結果變得有用，而不僅僅是令人難堪。被扣留的結果需要一個驗證工程師能夠檢查、重現和質疑的理由。
ARB3 讓這個問題變得無法忽視
我在 ARB3 中發現了最明確的失效案例，即合成仲裁器屬性 assert (g0 && g1) |-> (turn == 0)。在裸流程中，它是綠色的。當我打開其波形與可達性證據時，前件 g0 && g1 在該合成仲裁器中是不可達的。該蘊涵式僅在狹義上獲得了證明——即它從未被迫為其所描述的狀態負責。 前件從未被觸發。
當驗證儀表板一片綠意盎然時，這項區別說來容易，卻很難始終銘記於心。我最初將該蘊涵式解讀為對仲裁行為的斷言。可達性結果改變了我所看到的事實：這是一個觸發條件從未發生的主張。將其稱為 VACUOUS 比保留綠色標籤有用得多，因為它引導審查人員關注使該證明變得空洞的假設或激勵（stimulus）。
在制定策略標籤時，我反覆回到這個面板。 VACUOUS 聽起來可能是個苛刻的結果，直到你考慮了另一種選擇。如果簽核記錄保留了一項證明，卻未記錄其前件從未觸發，那麼審查就接收了一個缺乏賦予其意義之條件的結論。更好的記錄應當明確指出該限制，並留給人們具體的事實以供質詢。 該可達性記錄應當與判決並列。
我也必須克制將空洞性（vacuity）僅僅視為表面警告的想法。如果該屬性旨在約束仲裁條件，那麼不可達的觸發行為就是該屬性是否真正執行了預期行為的核心證據。儀表板不應要求審查人員從綠色結果中去推斷這一點，而應當保留可達性調查結果、將該結果導出證書路徑，並使下一步審查行動變得一目了然。
業界的現狀讓我更加意識到形勢的嚴峻。示範規範中引用的 2024 年 Wilson Research Group / Siemens EDA 研究報告指出，初次矽晶圓成功率（first-silicon success）僅為 14%。這不是 Veriprajna 的測量數據，這個合成看板也無意解釋該數字。但它確實讓我不再願意將令人愉悅的儀表板狀態本身視為證據。
管線屬性在理應捕獲的故障中倖存了下來
我在測試 PIPE3（一個合成兩級管線屬性）時遇到了第二個失效案例： assert v2 |-> (s2 == s2)。我原本想要一個簡潔的斷言範例，其讀起來合情合理，足以混過膚淺的審查。該後件（consequent）是一個同義反覆（tautology）。它宣稱 s2 等於其自身。 該後件沒有約束任何東西。
示範系統中的關鍵之處不僅僅在於從文字中發現同義反覆。治理閘門會注入相關的單點設計突變（single-point design mutations），並檢驗該屬性是否能擊殺它們。對於這個具有代表性的弱管線案例，PIPE3 記錄了 0/6 突變擊殺結果。該屬性在相關的故障變體中倖存了下來。這就是為什麼策略會賦予 WEAK，而不是允許裸 PROVEN 結果作為歸檔證據。 突變結果檢驗了有用的敏感度。
在試圖讓這個範例看起來不那麼顯而易見的過程中，我學到了一些令人不安的事實。人類可以讀到 s2 == s2 並迅速將其排除。但許多弱點不會如此直白地顯露出來。這就是為什麼我不希望示範系統依賴操作員去發現可疑字串。真正有用的產物是流程：可達性、相關突變擊殺測試、COI，以及記錄其原因的策略決策。
我逐漸將突變檢查視為一種嚴格拒絕過於討巧之證明解讀的規範化方法。其目的不是製造引人注目的失敗，而是詢問該屬性是否能察覺到它理應約束之行為中的相關局部變動。當它無法察覺時，結果會向審查人員提供可執行的資訊：在該斷言能夠支持簽核記錄之前，需要對其進行強化或走不同的審查路徑。
這也是為什麼該示範系統的基準測試需要嚴謹明確的界定。其本地 python -m backend.bench 運行在固定的已標註合成斷言集上評分為 18/18，並識別出 6 個示範系統自身無閘門基準線原會直接蓋章放行的證明。這些數據是對該示範系統標註治具的可重現性檢驗。它們不是生產環境中的比率，不是對 AI 編寫斷言的一般性斷言，也不是與商業形式化工具的對比。
我不再試圖讓閘門顯得寬鬆
在得到最初的審計結果後，我面臨一個設計抉擇：放寬被扣留的判決以使看板看起來更樂觀，或者讓看板拒絕證明它無法捍衛的項目。我選擇了後者，因為真正的簽核審查需要有能力區分完整證明與有界證明（bounded proof）、不可達前件與有意義的屬性，以及弱檢查與能對相關故障行為做出反應的檢查。 扣留是一種審查結果，而不是死胡同。
這項抉擇體現在策略詞彙中。TRUSTWORTHY 贏得已簽署的示範證書。BOUNDED-PROVEN、VACUOUS、WEAK、DEAD 與 VIOLATED 則保留了扣留該證書或呈報該結果的不同原因。例如在 CDC 治具中，較強的屬性 assert (req && !ack) |-> ##1 req 被判定為 VIOLATED 並產生具體的合成反例波形。它說明了事務遺失（lost-transaction）或 CDC 失效類別，但絲毫不代表客戶晶片的情況。
我並不認為這是為了取代驗證團隊現有引擎的宣傳。生產環境的方向是引擎無關的（engine-agnostic）：在現有的形式化工作流程周圍設置閘門，然後使其驗收標準變得可供檢查。真實引擎適配器與 RTL 讀取在本次示範中被延後實作。 所示範的邊界特意保持狹窄。 該邊界至關重要，因為它使主張與實際運行的內容保持相稱。
我現在要求判決旁必須附有憑據
我不斷思考在斷言編寫者獲得 AI 輔助時，簽核會議真正需要的產物是什麼。它不是來自編寫者的信心評分，而是一份記錄了執行了哪些檢查、可達性結果為何、擊殺了哪些突變、COI 包含什麼，以及策略為何允許或扣留認證的記錄。 審查需要能夠重新開啟檢驗的證據。
這正是示範系統在 signoff_certificate.json 中導出的內容：每個屬性的判決、可達性、突變結果、COI、適用情況下的反例記錄，以及 SHA-256 欄位。我將該證書構建為示範記錄，因為審查人員應該能夠重構該決策，而不是盲目相信綠色徽章。 證書應當保留通往其判決的路徑。
如果你寧願親眼觀看而非讀我的文字描述，這裡是整套系統端到端運行的完整過程。
我讓 該示範系統 可以實際運行，以便人們能夠檢查從 8/8 到 5/8 的逆轉，而不是將其作為口號反覆宣傳。我從中獲得的結論雖然謙遜卻歷久彌堅：值得歸檔的證明承載著它約束了什麼、在什麼情況下倖存，以及為何有人可以信賴它的證據。綠色依然有用，它只是需要一份能讓下一位審查人員決定其是否值得進一步採信的記錄。
