SystemVerilogアサーションを監査したとき、8つのグリーンなフォーマル証明は提出可能な5つになった
合成フォーマル検証ボードが8/8 PROVENと報告するのを見届け、さらにその監査で5/8のみをTRUSTWORTHYと認定するのを目撃した。この逆転こそが、AI生成SystemVerilogアサーション（SVA）向けガバナンスの実行可能なデモであるProof Firewallの前提であり、テープアウトサインオフレビューに到達する前に合格（グリーン）の証明が満たすべきだと私が考える基準を一変させた。
都合の悪い事例こそ可視化されるべきであるため、私は合成アービター、2段パイプライン、CDCクロッシング上でフィクスチャ作成の「LLM作成」プロパティを用いてこのボードを構築した。アサーションはプロパティ台帳上では何の問題もないように見えることがある。フォーマル検証エンジンは合格（グリーン）の結果を返すかもしれない。だが、その含意（インプリケーション）は実質的な検証作業を一度も行う必要がなかったか、あるいは関連する設計動作が破壊された後でもパスし続けている可能性がある。私はこれまでPROVENという言葉を到達点として扱っていた。このデモを構築したことで、それをエビデンスレビューの始まりとして捉えざるを得なくなった。
このProof Firewallデモは、フォーマル検証エンジンを置き換えたり、実際のRTLを取り込んだり、デフォルトパスでライブLLMを呼び出したりするものではない。意図的により小規模で検査しやすくなっている。純粋なPython明示的状態モデルチェッカーが合成遷移システムIRを評価し、その後ガバナンスゲートが前提条件の到達可能性、ミューテーションキル、および影響円錐（COI）をチェックする。出力は、署名付きデモ証明書を提出する根拠か、あるいは人間のレビューのために結果を保留する根拠のいずれかとなる。
最初は誤った種類のグリーンから始まった
最初のバージョンのボードがまさに完璧に整っていたため、安心感を覚えていたのを覚えている。8つのプロパティ、8つの緑のバッジ、そして作業が完了したかのように見せるベアフローの表示。私の当初の直感は、そのクリーンな結果をより分かりやすく説明するデモにすることだった。エンジニアリングの課題はプレゼンテーションにあると考えていた。証明を表面化させ、アサーションを示し、ダッシュボードをより信頼しやすくすることだと。グリーンという結果は本物だったが、レビューアーが問うべき問いよりも小さな問いにしか答えていなかった。
その後、私は同じ8つのプロパティを、実際の提出（ファイリング）の議論で求められるチェックにかけた。前提条件が真になることはあったのか？設計の関連部分が変更された場合にアサーションは異議を唱えるか？それは意味のあるCOIを制約しているか？これらの問いは、ソルバーが返した結果だけでなく、その証明が何を勝ち得たのかを問うため、緑のバッジほど耳障りの良いものではない。
私は構築の最初の枠組みを放棄せざるを得なかった。8/8 PROVENを示す画面はベアフローのベースラインの正確な表示ではあったが、サインオフのストーリーとしては不完全だった。ファイアウォール監査の後、同じ固定された合成ボードには5つのTRUSTWORTHYの結果、1つのVACUOUSの結果、そして2つのWEAKの結果が存在する。残りの3つが成功としてラベルを付け替えられることはない。それらはその理由を説明するエビデンスとともに保留される。証明ラベルと提出の決定は異なる成果物である。
ここで私は「ガバナンス」という言葉を慎重に選んだ。デモの決定論的チェックにより、提出の決定がレビュー可能になる。オプションのSVA作成者がアサーションを提案することはあっても、モデルチェッカーとポリシーゲートが判定を下す。エージェントが助言し、コードが決める。私は、不合格の結果が単に都合の悪いものではなく有用なものとなるよう、ゲートを十分にわかりやすくしようとした。保留された結果には、検証エンジニアが検査、再現、異議申し立てを行える理由が必要である。
ARB3によって問題を無視できなくなった
最も明白な不合格事例はARB3、すなわち合成アービターのプロパティであるassert (g0 && g1) |-> (turn == 0)に見られた。ベアフローではこれはグリーンである。その波形と到達可能性のエビデンスを開いたところ、前提条件g0 && g1はその合成アービターにおいて到達不能だった。この含意は、それが記述した状態に対して一度も応答を強いられなかったという狭い意味でのみ証明されていたにすぎない。前提条件が発火することは決してない。
その違いを言葉にするのは簡単だが、検証ダッシュボードがグリーンで埋め尽くされているときに常に意識し続けるのは難しい。私は当初、この含意を調停動作に関する主張として読んでいた。到達可能性の結果は、私が見ているものを変えた。それはトリガー条件が決して発生しない主張だったのである。これをVACUOUSと呼ぶことは、グリーンのラベルを維持するよりも有用である。なぜなら、証明を空虚なものにした仮定やスティミュラスへとレビューアーを導くからだ。
ポリシーラベルの作業をしている間、私は何度もこのパネルに立ち返った。VACUOUSは、その代替案を考慮するまでは厳しい結果のように聞こえるかもしれない。サインオフの記録が前提条件が決して発火しないことを記録せずに証明を保持する場合、レビューはその意味を与える条件を欠いた結論を受け取ったことになる。より優れた記録とは、制限を明示し、人間が具体的に精査できる材料を残すものである。その到達可能性の記録は判定の傍らにあるべきである。
また、私は空虚性（バキュイティ）を表層的な警告として扱う誘惑にも抗わなければならなかった。プロパティが調停条件を制約することを目的としている場合、到達不能なトリガー動作は、そのプロパティが意図した動作を行使したかどうかに関する中心的なエビデンスとなる。ダッシュボードはレビューアーにグリーンの結果からそれを推測させるべきではない。到達可能性の結果を保持し、その結果を証明書パスから除外し、次のレビューアクションを自明にする必要がある。
業界の背景が私にとっての危機感を強めた。デモの仕様書で引用されている2024年のWilson Research Group / Siemens EDAの調査では、ファーストシリコンの成功率が14%と報告されている。これはVeriprajnaによる測定値ではなく、この合成ボードがその数値を説明すると主張するものでもない。だがそれにより、私は快適なダッシュボードの状態それ自体をエビデンスとして扱うことに一層慎重になった。
パイプラインプロパティは検知すべき破壊をすり抜けて生き残った
2つ目の失敗に直面したのは、PIPE3（合成2段パイプラインプロパティ：assert v2 |-> (s2 == s2)）をテストしていたときだった。私は、表層的なレビューをすり抜けてしまうほどもっともらしく読めるアサーションの簡潔な例を求めていた。後件（帰結部）は恒真命題（トートロジー）である。それはs2がそれ自身と等しいと述べている。後件は何一つ制約していない。
デモにおける重要なステップは、文章の中でトートロジーを見つけることだけに留まらない。ガバナンスゲートは関連する単一箇所の設計ミューテーションを注入し、プロパティがそれらをキル（検知・排除）するかどうかを問いかける。取り上げられた脆弱なパイプラインのケースでは、PIPE3は0/6のミューテーションキル結果を記録する。プロパティは関連する破壊されたバリアントをすり抜けて生き残ってしまう。そのためポリシーは、WEAKを割り当て、単なるPROVENの結果が提出エビデンスとして通用することを許さない。ミューテーション結果は有用な感度をテストする。
この例をあまり自明に感じさせないようにする試みから、私は居心地の悪い教訓を得た。人間ならs2 == s2を読んで即座に却下できる。しかし、多くの弱点はこれほど明白に現れるわけではない。だからこそ私は、デモがオペレーターの怪しい文字列の見つけ出しに依存することを望まなかった。有用な成果物とはその手順である。すなわち、到達可能性、関連するミューテーションキルテスト、COI、そしてその理由を記録するポリシーの決定である。
私はミューテーションチェックを、証明に対する都合の良すぎる解釈を拒絶するための規律ある方法だと見なすようになった。目的は劇的な不合格を作り出すことではない。プロパティが制約すべき動作における関連する局所的な変化に気付くかどうかを問うことである。気付かない場合、その結果はレビューアーに行動可能な洞察を与える。すなわち、このアサーションがサインオフ記録を裏付ける前に、強化するか別のレビューパスを経る必要があるということだ。
これが、デモのベンチマークに限定的な説明が必要な理由でもある。ローカルのpython -m backend.benchの実行は、18/18のスコアを固定ラベル付き合成アサーションセットに対して記録し、6つの証明をデモ独自のゲートなしベースラインが無批判に承認したであろうものとして特定する。これらの数値はこのデモのラベル付きフィクスチャに関する再現性チェックである。本番環境の比率でも、AI作成アサーション全般に関する主張でも、商用フォーマル検証ツールとの比較でもない。
ゲートを寛容に見せようとするのをやめた
最初の監査結果の後、私には設計上の選択肢があった。保留された判定を和らげてボードをより楽観的に見せるか、あるいはボード自身が擁護できないものの認定を拒絶させるかである。私は後者を選んだ。なぜなら、実際のサインオフレビューには、完全な証明と有界（バウンデッド）な証明、到達不能な前提条件と意味のあるプロパティ、そして脆弱なチェックと関連する破壊動作に反応するチェックとを区別する能力が必要だからである。保留はレビューの結果であり、行き止まりではない。
その選択はポリシーの語彙に表れている。TRUSTWORTHYは署名付きデモ証明書を獲得する。BOUNDED-PROVEN、VACUOUS、WEAK、DEAD、そしてVIOLATEDは、その証明書を保留するか結果をエスカレーションするための異なる理由を保持する。たとえばCDCフィクスチャでは、より強力なプロパティであるassert (req && !ack) |-> ##1 reqがVIOLATEDとなり、具体的な合成反例波形を生成する。これはトランザクション喪失またはCDC故障クラスを例示している。顧客のチップについて何かを語るものではない。
私はこれを、検証チームの既存のエンジンを置き換えるための提案とは見ていない。本番に向けた方向性はエンジン非依存である。既存のフォーマルワークフローの周囲にゲートを配置し、その受け入れ基準を検査可能にすることだ。実エンジン向けアダプターとRTLの取り込みは、このデモでは保留されている。実証された境界は意図的に狭く保たれている。その境界が重要なのは、主張を実際に実行されている内容に見合ったものに保つためである。
今や私は判定の傍らに受領証（レシート）を求める
アサーション作成者がAIの支援を受けている場合、サインオフ会議で必要とされる成果物について私は考え続けている。それは作成者による信頼度スコアではない。どのチェックが実行され、到達可能性の結果がどうであったか、どのミューテーションがキルされたか、COIに何が含まれていたか、そしてなぜポリシーが認証を許可または保留したかを記した記録である。レビューには再検証可能なエビデンスが必要である。
それこそが、デモがsignoff_certificate.jsonでエクスポートするものである。すなわち、プロパティごとの判定、到達可能性、ミューテーション結果、COI、該当する場合の反例記録、およびSHA-256フィールドである。私がこの証明書をデモ記録として構築したのは、レビューアーが緑のバッジを盲信することなく、その決定を再構成できるようにするためである。証明書はその判定に至る経路を保持すべきである。
私の説明を読むよりも実際に見てみたいという方のために、エンドツーエンドで実行される全体をここに紹介する。
私はこのデモを実行可能にした。それは、8/8から5/8への逆転が単なるスローガンとして繰り返されるのではなく、実際に検査できるようにするためである。そこから私が得た教訓は控えめながらも揺るぎないものだ。提出に値する証明とは、それが何を制約し、何を生き延び、なぜ信頼できるのかというエビデンスを伴うものである。グリーンは依然として有用である。ただ、次のレビューアーがそれをさらに先へと進める価値があるかどうかを判断できる記録が必要なだけなのだ。
