🤖 AI

SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation

本論文は、推論に基づく反復評価、連鎖思考推論、および自己一貫性投票を通じて、LLM によって生成された SystemVerilog アサーションと自然言語仕様との意味的整合性を強化するフレームワーク SpecAlign を提示し、これによりゴールド RTL に依存することなくアサーションの精度を向上させるものである。

原著者： Jaime Rafael Imperial, Hao Zheng

公開日 2026-05-26

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Jaime Rafael Imperial, Hao Zheng

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

あなたが、新しい複雑な家のための詳細な設計図を描いた熟練した建築家（設計仕様）だと想像してください。あなたは、非常に速く、非常に創造的だが、時折夢見がちな現場監督（大規模言語モデル、または LLM）を雇って、その家のための安全規則のリストを作成させたいと考えています。これらの規則は、**SystemVerilog アサーション（SVA）**と呼ばれる厳格で技術的なコードで記述されます。

問題は、この現場監督は安全規則のように見え、文法チェックも通る文章を書くのが得意ですが、彼が書く規則の中には実際には無意味なものや、あなたの元の設計図と矛盾するものが含まれることがあるという点です。

例えば、あなたの設計図には「警報が作動している間は、玄関の鍵が施錠されなければならない」とあります。しかし、現場監督は「玄関の鍵が作動している間は、玄関の鍵が施錠されなければならない」という規則を書くかもしれません。これは規則のように聞こえ、コンピュータは「はい、それは有効な文です」とさえ言うかもしれませんが、現実世界では意味をなしません。

問題：「有効」だが誤っている

従来、これらの規則が良し悪しを判断するためには、エンジニアは家の物理的なモデル（ゴールデン RTLと呼ばれる）を構築し、そのモデルに対して規則を実行していました。もし規則がモデルを破損させなければ、それは良いと仮定されていました。

しかし、この論文は、特定のモデルに適合するかどうかを見るだけで規則が機能するかどうかをチェックするのは、モデルが完璧であれば素晴らしいが、もしモデルがまだ存在しない場合はどうなるのか、あるいはその特定のモデルに対して技術的に「真」であっても、あなたが求めたことの要点を完全に欠落している場合はどうなるのか、と主張しています。現場監督は、賢く聞こえるが役に立たない規則を幻覚として生成している可能性があります。

解決策：SpecAlign

著者たちは、SpecAlignという新しい「品質管理」フレームワークを導入しました。規則をテストするために物理的なモデルを構築する代わりに、SpecAlign は超スマートな翻訳者と事実確認者のように機能し、現場監督の規則をあなたの元の設計図（自然言語仕様）と直接比較します。

SpecAlign がどのように機能するかを、簡単な比喩を使って説明します。

1. 翻訳ステップ（正規化）

現場監督は厳格なコード（SVA）で規則を書きます。SpecAlign はまず、これらを平易な英語に翻訳します。

比喩: 現場監督が「建築コード」で書いていると想像してください。SpecAlign はそれを「英語」に翻訳し、あなたの英語の設計図と直接比較できるようにします。

2. 二段階の事実確認（アライメントループ）

SpecAlign は 2 回のチェックを実行します。

ラウンド 1（プロパティチェック）: 現場監督があなたの設計図から抽出したアイデアをチェックします。これらのアイデアはあなたが書いた内容と一致していますか？
ラウンド 2（規則チェック）: 実際の翻訳された規則をチェックします。それらはアイデアとあなたの設計図に一致していますか？

3. 「3 つの箱」による判定

単に「合格」または「不合格」と言うのではなく、SpecAlign はすべての規則を 3 つの箱のいずれかに分類します。

🟢 包含（緑）: 規則はあなたの設計図と完全に一致します。「はい、これはあなたが求めたものです。」
🔴 矛盾（赤）: 規則はあなたの設計図と直接対立します。「いいえ、あなたは警報が作動しているときに鍵が施錠されると言いましたが、この規則は施錠解除されると言っています。」
⚪ 不明（灰色）: 規則はあなたの設計図で言及されたことのないものを言及しています。「あなたは『スマートロック』について言及しましたが、あなたの設計図には単に『ドア』としか書かれていません。この追加機能が良しとされるかどうかはわかりません。」

4. 「自己修正」ループ

規則が**赤（矛盾）**の箱に入ると、SpecAlign はそれを単に捨て去るわけではありません。厳格な編集者のように機能します。

規則がどこで間違えたかを現場監督に正確に伝えます。
設計図に基づいて規則を書き直すよう現場監督に求めます。
新しい規則を再度チェックします。
規則が緑になるか、少なくとも明確に灰色になるまでこれを繰り返します。

「編集者」が間違いを犯していないことを確認するために、SpecAlign は AI に 3 つの異なる方法で問題を考えて（3 人の異なる専門家のように）から、最終的な答えについて投票させます。これは自己一貫性と呼ばれます。

結果：混乱の整理

著者たちは、この手法を 2 つの現実世界の設計（チップ間の通信プロトコルなど、USB やネットワークカードがコンピュータと通信する仕組みに類似したもの）でテストしました。

SpecAlign 以前: 競合する手法は数百の規則を生成しました。そのほとんどは、赤（設計図と矛盾する）または灰色（詳細を捏造する）でした。緑（実際に設計図と一致する）はごくわずかでした。
SpecAlign 以降:
- 赤（矛盾する）規則の数が劇的に減少しました。ある設計では、148 件の不良規則がわずか 6 件にまで減りました。
- 緑（整合する）規則の数が大幅に増加しました。
- 灰色（不明）規則の数が増加しました。なぜか？ SpecAlign は、捏造された詳細を含む規則を「良い」として偽装することをやめたからです。それらを「これが良いと言えるほど情報が不足している」と正しく識別しました。

大きな教訓

この論文は結論として、規則が文法的に正しいか、コンピュータのテストに合格するからといって、それがあなたが思っている意味を持っているわけではないと述べています。

SpecAlign は、物理的なモデルを最初に構築することなく、AI が実際にあなたの指示に耳を傾けているかどうかを確認する方法を提供します。それは、「技術的には有効だが役に立たない」規則の山を、実際に信頼できるより小さく整理された規則のセットに変換し、同時に確信を持てない曖昧なものを明確にマークします。

技術的サマリー：SpecAlign – システムVerilog アサーション生成のための意味的整合フレームワーク

1. 問題定義

現代のハードウェア設計の複雑化に伴い、アサーションベース検証（ABV）を支援するため、システムVerilog アサーション（SVA）を生成する大規模言語モデル（LLM）の採用が進んでいます。しかし、既存の LLM 手法は主に構文の妥当性と形式検証（FV）の結果（例えば、与えられた RTL 上でアサーションが証明されるか、または反例を生成するか）に焦点を当てています。これらの指標は、生成されたアサーションが自然言語仕様で記述された動作意図を正確に反映しているかどうかという意味的整合性には対処していません。

LLM は、構文的に正しく特定の RTL 実装上で形式的に証明可能であっても、意味的に無効であったり幻覚（ハルシネーション）を含んでいたりするアサーションを生成する可能性があります。例えば、あるアサーションはプロパティをトリガーする同じエッジでクロックをサンプリングするものであり、FV を通過したとしても空虚（vacuous）な結果となる場合があります。「ゴールド」RTL モデルが比較対象として存在しない場合、このようなアサーションの手動検査は時間がかかり、信頼性を低下させます。さらに、FV エンジンは複雑な設計に対して生成されたアサーションの大量セットを評価する際に、状態空間の爆発というスケーラビリティの問題に直面します。RTL 実装の詳細に依存せず、仕様自体に対する意味的一貫性を評価するフレームワークが緊急に必要とされています。

2. 手法：SpecAlign フレームワーク

SpecAlign は、ゴールド RTL に依存することなく、LLM によって生成された SVA を評価し、反復的に洗練させることを目的とした仕様中心のフレームワークです。これは、プロパティ整合ループとSVA 整合ループという 2 つの主要な反復ループを通じて動作します。両方のループは、整合性チェック、不一致分析、および証拠抽出という 3 つの中核段階を利用します。

A. 概要

このフレームワークは、設計意図の異なる表現間の比較を正規化します。入力には自然言語のプロパティ（ $P$ ）と生成された SVA（ $A$ ）が含まれますが、フレームワークは特定の抽出プロセスを通じて、すべての SVA を**自然言語サマリー（ $N$ ）**に変換します。この正規化により、プロパティとアサーションの両方を、設計仕様（ $S$ ）に対して同じ意味レベルで評価することが可能になります。

B. 中核コンポーネント

整合性チェック:
- 分類: フレームワークは、仕様との関係に基づいて、自然言語の説明（ $X_i$ $X_{i}$ ）を 3 つのカテゴリに分類します。
  - Entails（帰結）: すべての要素が仕様によって支持されている。
  - Contradicts（矛盾）: 少なくとも 1 つの要素が仕様と矛盾している。
  - Unknown（不明）: 要素が支持も矛盾もしていない（多くの場合、仕様には存在しない実装固有の仮定による）。
- 自己整合性投票: 信頼性を向上させるため、システムは Chain-of-Thought（CoT）プロンプト戦略を採用します。特定の入力に対して $k$ 個の推論パスを生成し、多数決を用いて部分判定を集約します。同点の場合、保守的な優先順位が適用されます：Contradicts > Unknown > Entails。
- 参照選択: プロパティループは設計仕様（ $S$ ）を参照として使用します。SVA ループは、散在する仕様ドキュメントからのノイズを低減するために「整合済みプロパティバンク」（利用可能な場合）を使用し、そうでない場合は $S$ にフォールバックします。
不一致分析と洗練:
- 判定がContradictsの場合、システムは不一致分析を実行します。説明内の特定の矛盾要素を特定し、仕様内の正しい動作を参照し、構造化された実行可能なフィードバック（ $F_i$ ）を生成します。
- このフィードバックは、LLM がプロパティまたはアサーション（ $P'_i$ または $A'_i$ ）を再生成するよう導き、トリガー条件を明示的に定義し、仕様には存在しない新しい信号や動作を導入しないようにします。
- 洗練された出力は、固定された反復回数に達するか、出力が整合するまで、整合ループ内で再評価されます。
証拠抽出:
- Entailsの場合、システムは仕様から支持証拠（引用と場所）を抽出し、人間のレビューを容易にし、信頼性を強化します。
- Unknownの場合、システムはどの要素が曖昧または未定義かを分類し、真の矛盾と仕様不足の動作を区別します。
定量的指標:
- フレームワークは、特定の反復段階における帰結されたアサーション数（ $E$ ）の総アサーション数（ $n$ ）に対する比率として計算される**整合スコア（ $a_t$ ）**を定義します（ $a_t = E/n$ ）。洗練プロセスの目標は、このスコアを最大化することです。

C. 自然言語サマリーの抽出

重要な前処理ステップとして、形式的な SVA を構造化された自然言語サマリーに変換することが含まれます。LLM には、特定の SVA コンポーネント（トリガー、先行項、含意演算子、後続項、Disable If）を特定し、同等の自然言語フレーズにマッピングするようプロンプトが送られます。これにより、形式的コードの意味的意図が比較のために保持されます。

3. 主な貢献

本論文は、以下の貢献を概説しています。

意味的評価フレームワーク: ゴールド RTL に適用された形式検証に依存することなく、自然言語仕様に対して LLM 生成 SVA を評価するための新規アプローチ。
反復的洗練パイプライン: 既存の LLM ベースの生成ワークフローへの統合を目的とした、整合性チェック、不一致分析、および SVA サマリー抽出からなる構造化フレームワーク。
定量的整合メトリクス: 仕様の一貫性を測定するための意味的帰結分類に基づく整合スコアリングメトリクス。従来の FV 妥当性評価に代わるスケーラブルな代替手段を提供する。
不一致分析メカニズム: 矛盾するプロパティおよびアサーションに対する具体的かつ実行可能なフィードバックを生成する方法。手動レビューと自動洗練の両方を支援する。
実証的検証: 意味的洗練を通じて APB および UART 設計における矛盾するアサーションを削減した実験結果。

4. 実験結果

著者は、SpecAlign を 2 つのハードウェア設計、すなわちAPB（APB から I2C インターフェース）とUART（UART からバスインターフェース）で評価しました。フレームワークは、知識グラフを使用し RTL を生成に組み込むベースライン手法であるAssertionForgeと比較されました。

APB 結果:
- ベースライン（AssertionForge）: 442 個の SVA を生成し、整合スコアは0.02でした。帰結されたものは 8 件のみで、148 件が矛盾していました。
- SpecAlign: 442 個の SVA を維持しましたが、整合スコアを0.15に向上させました。重要なのは、矛盾するアサーションの数が0に減少し、帰結されたアサーションが 66 件になったことです。残りの 376 件は Unknown と分類されました。
UART 結果:
- ベースライン: 325 個の SVA を生成し、整合スコアは0.06（帰結 21 件、矛盾 142 件）でした。
- SpecAlign: 319 個の SVA を生成し、整合スコアは0.28でした。矛盾するアサーションは6件に減少し、帰結されたアサーションは 92 件に増加しました。

結果の分析:
実験により、ベースライン手法は仕様と矛盾するか、自然言語仕様には見られない実装固有の詳細（RTL）に強く依存するアサーションを生成する傾向があることが明らかになりました。SpecAlign はこれらの矛盾を効果的にフィルタリングします。SpecAlign における「Unknown」分類の増加（例：APB で 376 件）は失敗として解釈されるのではなく、実装固有の仮定を仕様で支持される動作から分離する、より保守的で正確な分類戦略として解釈されます。この区別は、サポートされていない動作を誤って「帰結」としてラベル付けする偽陽性を防ぎます。

5. 意義と主張

本論文は、SpecAlign が従来の形式検証に対するスケーラブルな補完を提供すると主張しています。意味的正しさを RTL 証明結果から分離することで、形式検証だけではアサーションが仕様で記述された意図された動作を捉えているかどうかを判断できないという限界に対処します。

著者は、形式検証が RTL 上でアサーションが成立することを証明するために必要である一方で、アサーションの意図の質を評価するには不十分であると強調しています。SpecAlign は以下の点により、LLM 生成アサーションへの信頼性を向上させます。

形式ツールが見逃す可能性のある意味的不整合（例：空虚な真理）を検出する。
RTL シミュレーションや形式証明前に矛盾を特定することで、デバッグの労力を削減する。
ゴールドモデルを必要とせずにアサーションを反復的に洗練するメカニズムを提供する。

論文は控えめに結論付けており、フレームワークは整合性を向上させるものの、分類手法の洗練、構文エラーのより良い捕捉、RTL 生成やデバッグなどの他のハードウェア設計自動化タスクへの手法の拡張など、今後の研究が必要であると述べています。