TensorEQC: Structure-Aware Equivalence Checking with GF(2) Algebra, Exact Tensor Networks, and Reset Analysis : a Multi-Algorithmic Study of Datapath Verification and Reset-State Dependence

技術要約：TensorEQC – 構造認識型等価性検証

問題提起
等価性検証（EC）は、回路の表現形式に対して非常に敏感である。異なる回路構造（例：XORが豊富なネットワーク、キャリーチェーン、有限体乗算器、整数乗算器など）は、それぞれ異なる検証手法を好む特有の構造的性質を示す。単一の手法（ブール代数、決定グラフ、テンソルネットワークなど）が、あらゆる回路タイプに対して普遍的に優位に立つことはない。さらに、シーケンシャル回路の検証においては、初期状態への依存性と、特定の観測境界内で解消される不確実性を区別する必要がある。これは特に、リセット状態に関して重要である。

手法
本論文では、単一のモノリシックなソルバーではなく、マルチアルゴリズム・ポートフォリオとして設計された実行可能な研究ワークフローであるTensorEQCを紹介する。その核心となる哲学は、エンジンは自身の正確なセマンティクスに従って検証義務を履行できる場合にのみ、その義務を完了させるべきであり、そうでなければその義務を別のエンジンに引き継ぐべきであるというものである。

このワークフローは、主に以下の3つのコンポーネントで構成されている：

1. 組合せ論的ポートフォリオ（Combinational Portfolio）： 出力が解消されるか、あるいはリソース制限に達するまで処理を行う、検証エンジンの逐次的なパイプライン。このパイプラインには以下が含まれる：
   • 構造ハッシング（Structural Hashing）： サポートされているプリミティブ（AND, OR, XORなど）の下で、式DAGの同一性を、可換正規化を用いて確立する。
   • シミュレーション（Simulation）： ランダム、全ゼロ、全一のパターンを用いたパックド・シミュレーションを使用し、負の証拠（反例）を見つける。
   • 代数的標準形（ANF）： ブール関数をGF(2)上の多項式として表現する。非ゼロの多項式から正確な負の証拠を生成するための特定の補題を利用する。
   • 関係テンソル除去（Relational Tensor Elimination）： ゲートをブール指示テンソルとして表現する。GF(2)の総和（パリティを計算する）ではなく、ブール半環上の論理和（充足する割り当ての存在を保持する）による変数消去を実行する。
   • ROBDDおよび全探索フォールバック（ROBDD & Exhaustive Fallback）： ノードキャップを備えた順序付き二分決定グラフ（OBDD）と、最終的なフォールバックとしての小規模サポートの全探索列挙を使用する。
2. テンソル・トレイン（TT）解析： 真理値表から正確なTT表現を構築し、代数的ランクを測定してゼロ関数をテストするコンパニオン・モジュール。GF(2)上のランクと実数上のランクを区別し、GF(2)のランクが大幅に小さくなり得ることを指摘する。
3. リセット解析： 明示的な状態を用いた自己合成（self-composition）を使用し、初期状態への依存性をチェックする同期モジュール。リセット依存性が直ちに観測可能であるケースと、特定の「フラッシング」サイクルの後に消失するケースを区別する。

主な貢献

• 正確なエンジンの統合： 構造ハッシング、GF(2)代数、関係テンソルネットワーク、およびROBDDを実用的に統合し、それぞれが明確な証明契約（proof contract）を維持していることを示す。
• 構造認識型戦略： 検証効率は回路構造と変数順序に強く依存するという経験的な証拠を提供する。例えば、インターリーブされた加算器のオペランドは低いテンソルランク（≤3）を示すが、分割されたオペランドは高いランク（129）を示し、後者はテンソルベースのアプローチには適さない。
• リセット状態の診断： 同期設計における真の初期状態依存性と、過渡的な不確実性を明示的に区別する方法を提供する。
• 再現可能な検証： 本論文には、5つの16入力関数を用いて、正確なGF(2)テンソル・トレイン構築、ランク測定、およびゼロ関数テストを検証する、自己完結型の新しい補足資料が含まれており、パリティの相殺と実際のゼロ関数の区別を裏付けている。

実験結果
研究では、2つの異なるエビデンス・セットについて報告している：

1. 歴史的ポートフォリオ・キャンペーン (v1.0.0)： このデータセットには、2,048ビットのリップル加算器、128ビットの多項式基底乗算器、およびアフィンネットワークを含む89件のケースランが含まれる。
   • 成功例： フルフローは、2,048ビットのリップル加算器（2.87秒）および128ビットのGF乗算器（0.80秒）の検証に成功し、特定のケース（BDDが解決できなかった2,048ビット加算器など）においてBDDのみのアプローチを上回った。
   • 限界： 1,024ビットのリップル加算器および1,024入力のアフィンネットワークにおいて、リソース制限（ノードキャップ、幅のキャップ）に達した。整数乗算の結果は、ANFの増大とテンソルのスコープ・キャップのため、10ビットに限定された。
   • 観察： フルフローは、最適なエンジンを直接選択する場合と比較してオーバーヘッドが発生することがあり、自動化と効率性の間のトレードオフを浮き彫りにした。
2. 新しい再現可能な補足資料： 5つの16入力関数（パリティおよびGF乗算を含む）に焦点を当てた集中実験により、正確なテンソル・トレイン構築とランク解析が小規模な関数に対して実現可能であることを確認した。また、GF(2)のスカラ和がゼロであっても、それがゼロ関数を意味しない（パリティの相殺）ことを検証し、TTのゼロテストによって正しく処理されることを示した。

意義と主張
本論文は、自らの貢献を普遍的な解決策ではなく、範囲を限定した技術的評価として明確に位置づけている。

• 普遍的な優位性の不在： 結果は、テンソルネットワークが他のすべての手法よりも優れているという主張を支持するものではない。代わりに、数学的ドメイン（例：低次有限体関数に対するGF代数、キャリーチェーンに対する関係的除去）に基づいて異なるエンジンを選択するという「表現感受型戦略」を支持している。
• 置き換えではなく統合： 中心的な成果は、正確な代数、関係的除去、決定グラフ、および時間的推論を、それぞれの証明契約を明確に保ちながら統合することに成功した点にある。
• 明示的な境界： 著者は、現在の実装がバイナリの組合せ論的プリミティブおよび小規模な同期マシンに限定されていることを強調している。これは、一般的なSystemVerilog、パワーアウェア・セマンティクス、非同期タイミング、または産業規模のネットリストをまだサポートしていない。また、論文では「証明（エンコードされたブール義務の正確な充足）」と「サーティフィケーション（検証済みのフロントエンドおよび証明チェッカーのチェーンを必要とするもの）」を区別しており、後者は将来の課題として記されている。

要約すると、TensorEQCは、ヘテロジニアスなロジックを扱うために複数の正確な検証手法を組み合わせるフレームワークを提供しており、単一のエンジンが普遍的に最適であることはないものの、構造化されたポートフォリオが特定の回路クラスを効果的に検証しつつ、その限界を明確に特定できることを示している。