大規模言語モデルは、チップ設計検証における最も煩わしい作業の一つ、すなわち自然言語で書かれた仕様を、RTL実装の正しさを判定するために利用できる形式的プロパティの集合へ変換する作業を実行する段階に近づいている。Semiconductor EngineeringでBrian Baileyが行ったインタビューは、現在のツールが有用な初期ドラフトを生成できる一方、集中的なエンジニアリングレビューなしに採用できる完全な集合を作成するには、なお遠いことを示している。
この進展が重要なのは、プロパティの記述が長年、形式検証におけるボトルネックとなっているためである。検証環境に組み込まれるとassertionsとして知られるSystemVerilogプロパティは、信号間の論理的・時間的関係を記述する。例えば、リセット動作、ハンドシェイク、one-hot条件、基本的な安全性チェックなどである。これらのプロパティが完全かつ正確であれば、設計の構築方法に依存せず、RTL実装の動作を仕様と比較するために利用できる。
現在、ツールにできることは何か？
大規模言語モデルを基盤とするツールは、仕様書、プロトコル標準、さらにはRTL内のコメントを読み取り、SVAプロパティのドラフトを提案できる。Axiomiseの最高経営責任者であるAshish Darbariは、仕様があまり頻繁に変更されない安定した標準に基づいている場合、この利用方法はより実用的になると述べている。この場合、ツールは検証プロセス全体を担うのではなく、初期コードを記述する反復的な部分を軽減する。
一部の手法では、knowledge graph、すなわちエンティティとその関係を保存する知識グラフを作成することで、モデルの精度向上を試みている。ノードには信号、モジュール、要件、ポートなどを含めることができ、エッジは「駆動する」「リセットする」「〜に応答する」といった関係を表す。要求に関連して見えるテキスト断片を検索する代わりに、システムは特定の事実やリンクを参照できるため、信号名を捏造したり、設計コンポーネント間の関係を誤解したりする可能性を低減できる。出典は、この文脈でCohenとChibaniによるRAG-SVA in the Landscape of LLM-Based Assertion Generationという研究に言及している。
問題はAIより前に始まっている
ツールは、そもそも記述または決定されていないものを抽出することはできない。SynopsysのアプリケーションエンジニアリングディレクターであるRavindra Anejaは、理想的な仕様は過去30年間にわたって利用可能なものではなかったと述べている。多くの場合、文書化が完了する前に開発が始まり、特に派生設計や作業中に要件が変化する場合など、一部のプロジェクトには完全な仕様が存在しないこともある。
この問題は表現だけでなく、変更管理にも関わる。マーケティングチームが新機能を追加したり、既存要件を変更したりする場合、設計チームと検証チームはその変更の影響を特定しなければならない。Siemens EDAのシニアバイスプレジデント兼ゼネラルマネージャーであるAbhi Kolpekwaは、仕様をプロパティへ変換するには、変更の履歴と文脈を追跡する「コンテキストインテリジェンス」が必要であり、毎回新しいテキストを生成するエージェントだけでは不十分だと考えている。
誤った信頼感のリスク
現在のアプローチにおける最大の制約は、プロパティが構文的には正しく、コンパイルされ、検証ツールによる証明に成功しても、実際に意図された動作をテストしていない可能性があることだ。Darbariは、弱いプロパティやvacuousなプロパティは、多くの動作を許容するため、誤った信号を使用するため、あるいは前提条件が欠落しているか過度に制約されているため、容易に成功する可能性があると警告している。したがって、「緑色の証明」は設計に誤りがないことを意味しない。証明は、証明されたプロパティ以上に強いものではない。
出典はさらに、モデルはアーキテクチャ上の意図やルールが存在する理由を理解するよりも、構造的・構文的なカバレッジでより良い性能を示す傾向があると述べている。そのため、モデルによる仕様の不正確な解釈が、形式的で厳密に見える一方、要件上のギャップを隠す記述へと変わる可能性がある。このギャップがFMEDA、セーフティファイル、ISO 26262およびISO 21434に関連する認証証拠などへ引き継がれれば、その影響は元の検証プロジェクトをはるかに超える可能性がある。
設計と検証の分離も問題となる。Normal Computingの製品設計リーダーであるKaye Maoは、エージェントがプロジェクト資料のどこまでにアクセスできるかを制限する必要があると指摘している。エージェントが設計そのものを使ってテストケースを生成することを許せば、検証プロセスの独立性が損なわれる可能性があるためだ。
実際には何が変わるのか？
Darbariによれば、AIは初期ドラフトの準備時間を数日から数分へ短縮できるが、その後の作業量を倍増させる可能性がある。生成された各プロパティには、仕様との照合、カバレッジ分析、vacuityのテスト、設計信号との関係のレビューが必要であり、失敗した場合には波形解析が必要になることもある。プロパティの数が10倍に増え、各プロパティに必要な精査の水準が変わらなければ、レビュー負担が高速生成による利益を上回る可能性がある。
certi.newsの観点では、本当の変化は検証エンジニアの置き換えではなく、中心をプロパティの記述から、その評価と出所の追跡へ移すことにある。Darbariは、生成されたプロパティを承認済みの成果物ではなくドラフトとして扱い、regression suiteに導入する前にレビューゲートを設けることを推奨している。また、エンジニアが適合性を確認できるよう、各プロパティの出典、すなわち仕様の段落、要件、またはそのプロパティを生成したRTL要素を記録すべきである。
Normal Computingの検証ソリューションエンジニアであるYaron Ilaniによれば、このアプローチはformal verificationを利用したい検証エンジニアにとっての参入障壁を下げる可能性がある。しかし、投資収益率の問題が解決されるわけではない。Kaye Maoは、エージェントの出力を検証する時間をコストに含める必要があると考えている。一方、Normal ComputingのソリューションチーフエンジニアであるArvind Srinivasanは、スケール拡大は計算能力だけの問題ではなく、データの完全性と人間によるレビューのコストにも関わると指摘している。
結論として、大規模言語モデルはプロパティ定式化における自動的で反復的な部分を高速化できるようになったが、仕様の完全性と設計意図の理解という二つの問題はまだ解決していない。これらのツールの価値は、モデルが生成できるプロパティの数ではなく、設計を理解するエンジニアの存在、ならびにカバレッジを独立して測定し、空疎または不適切なプロパティを検出する仕組みに左右され続ける。