Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification

技術サマリー：エージェント型 AI に基づく形式検証における欠落したリンクとしてのナレッジグラフ

問題定義
大規模言語モデル（LLM）は、自然言語仕様がシステムベリログアサーション（SVA）を生成し形式検証（FV）を加速する可能性を示しているが、依然として重大な障壁が存在する。主な課題は「グラウンディング」問題である：仕様は往々にして曖昧または不完全であり、重要なマイクロアーキテクチャの詳細はレジスタ転送レベル（RTL）コードに存在する。既存のアプローチは通常、仕様と RTL を緩く構造化されたテキストとして扱うため、仕様から RTL へのグラウンディングが脆弱となる。その結果、意味的な不一致、形式パース中の頻発する構文エラー、そして広範な反復修正と手動トリアージを必要とするアサーションが生じる。さらに、先行手法はしばしば、カウンターエグザンプル（CEX）やカバレッジレポートなどの形式ツールからのフィードバックを生成ループに永続的に統合することに失敗しており、体系的な洗練を制限している。

手法
著者は、意図と実装の間のギャップを埋めるために、構造化された中間表現（IR）からナレッジグラフ（KG）を構築する検証中心の手法を提案する。ワークフローは、入力、型付き JSON IR、ランタイム KG、およびエージェント編成の 4 層に整理される。

1. 中間表現（IR）： システムはデータを抽出し、型付き JSON アーティファクトに正規化する。これには、階層的な仕様を含む spec_chunks.json、requirements.json、階層や信号などの RTL メタデータを含む design_model.json、properties.json、および検証結果（formal_results.json、cex_cases.json、coverage_metrics.json）が含まれる。
2. ナレッジグラフ構築： これらの IR はノードとエッジとしてエクスポートされ、NetworkX を使用してランタイム KG を構築する。KG はアーティファクトレジストリとして機能し、要件、設計階層、信号、仮定、およびプロパティをリンクする。これは限定されたコンテキストの検索を可能にする。例えば、プロパティを生成する際、KG は特定の要件、その親仕様フラグメント、関連する RTL 信号、およびルールブックを提供する。
3. マルチエージェント編成： 検証プロセスは、KG をクエリおよび更新する専門エージェントに分解される。
   • プロパティ生成： リードエージェントが、要件を分解する spec_analyst、SVA 構文を合成する sva_author、準拠を検証する sva_reviewer、およびフィードバックに基づいて修正する sva_patcher を調整する。
   • 構文修正： 専用のループがコンパイルエラーを処理する。エージェントは診断を分析し、未宣言の識別子などの一般的なパターンに対して決定論的な修復を適用し、RTL 宣言や要件テキストなどの複雑なコンテキストを使用してより困難なエラーに対処する。プロパティには最大 3 回の修正試行が許可される。
   • CEX 修正： プロパティが失敗した場合、エージェントは VCD ウェーブフォームと失敗トレースを解析する。spec_assertion_analyzer が根本原因（例：RTL バグ対不足仕様）を分類し、cex_fixer が制約を調整するかアサーションを強化する。
   • カバレッジ改善： エージェントはカバレッジ指標を分析して、アクセス不能なコードや空虚なプロパティを特定し、ギャップを埋めるためのターゲット型プロパティを生成する。

主な貢献
本論文は 3 つの主要な貢献を主張する。

1. 検証中心の KG 構築： 仕様意図、RTL 構造、生成されたプロパティ、および形式ツールの結果を単一のクエリ可能なアーティファクトに統合する、構造化された IR から KG を構築する新規アプローチ。
2. トレーサビリティを備えたマルチエージェントワークフロー： エージェントが KG にグラウンディングされたコンテキストを使用して SVA を生成・洗練し、要件から設計要素、プロパティ、および検証結果への明示的な追跡リンクを維持するシステム。
3. 実証的評価： 7 つのオープンソースベンチマーク設計における評価により、KG にグラウンディングされたコンテキストがプロパティ生成の有効性、構文的妥当性、および CEX 洗練ループの効率性に与える影響を定量化した。

結果
本手法は、GPT-5.2 モデルおよび Cadence JasperGold を使用して、7 つの設計（FIFO、Lemming、ALU、CICD、BST、TTC カウンタ、および CSR）で評価された。

• 構文とコンパイル： このアプローチは、低コストの構文修復オーバーヘッドでコンパイル可能な SVA を一貫して生成した。特に design_model IR による信号と階層の決定論的解決による KG にグラウンディングされたコンテキストは、未宣言の識別子などのフロントエンドの問題を大幅に減少させた。
• 形式カバレッジ： ベンチマーク全体で、エンドツーエンドの形式カバレッジは 78.5% から 99.4% の範囲であった。
• 洗練の効率性： FIFO や CIC デシメータなどの設計は、CEX およびカバレッジループ後に著しい改善を示し、多くの初期失敗は、取得されたコンテキストを通じて修正可能なローカルな問題（欠落したガード、境界条件など）に起因することを示唆している。
• 限界： 収束は設計に依存した。バイナリサーチツリー（BST）のような複雑な設計や、グローバル不変条件や深い時間的推論を必要とする設計（例：Lemming、ALU）は、自動修正からの改善が限定的であった。著者は、現在の LLM の能力は複雑な時間的および算術的推論に苦慮しており、意味的デバッグがより困難なベンチマークにおける主要なボトルネックであると指摘している。

重要性
本論文は、提案された KG 中心のアプローチが先行研究の決定的な弱点、すなわち要件、RTL 意味論、および検証結果間の構造化されたクエリ可能なリンクの欠如に対処すると主張する。形式ツールのフィードバック（CEX、カバレッジギャップ）を一時的な出力ではなく、永続的かつクエリ可能な KG コンテンツとして扱うことで、システムは閉ループの洗練プロセスを可能にする。著者は、複雑な推論に対する意味的修正が依然として課題である一方、このフレームワークはトレーサブルで設計にグラウンディングされたプロパティ生成のための堅牢な基盤を提供すると結論づけている。LLM の能力が進歩するにつれ、これら KG が提供する構造化されたコンテキストとトレースを活用する立場が強化され、自動化された形式検証の信頼性がさらに向上するであろう。