合成ボード上での証明レビューの実例
すべての画像は稼働中の合成デモのスクリーンショットです。ボードは最初に8件のPROVENベアフロー結果として始まり、その後監査によって保留された証拠が可視化されます。
監査により3件のグリーン結果が覆る
Tape-Out Sign-Off Boardは、ベアフロー表示において当初8/8 PROVENを示します。ファイアウォール監査の後、5/8がTRUSTWORTHYとして認証されます。残りの3件は1件のVACUOUSと2件のWEAKプロパティです。これは固定された合成フィクスチャであり、顧客の設計や商用エンジンの結果ではありません。
トリガーが決して発生しないため、ARB3は何も証明していない
合成ARB3アサーションである assert (g0 && g1) |-> (turn == 0)は、合成アービター内で前件が到達不能であるためVACUOUSです。この結果は、証明された含意であっても何も保証できない場合がある理由を示しています。
PIPE3は検出すべきミューテーションを生き残ってしまう
合成PIPE3アサーションである assert v2 |-> (s2 == s2)はWEAKです。その恒真的な後件は注入された関連ミューテーションを生き残り、注目パイプラインケースでは0/6のミューテーションキルを記録します。
より強力なCDCプロパティは独自の反例を示すことができる
合成弱CDC2プロパティはWEAKです。これを assert (req && !ack) |-> ##1 req へと強化すると、合成CDCフィクスチャ上でVIOLATEDとなり、具体的な反例波形を生成します。これはトランザクション喪失というCDC障害クラスを示すものであり、実チップに関する主張ではありません。
レビューは構造化された記録を残す
署名付きデモ証明書には、各プロパティの判定、到達可能性、ミューテーション結果、COI、および該当する場合は反例レコードに加え、SHA-256フィールドが記録されます。これにより、レビュアーがステータス変更の理由を推測する必要なく、監査内容をレビュー可能にします。
