Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement

スマートフォンから宇宙船に至るまで、あらゆるものに電力を供給するために数十億個のトランジスタがオンとオフを繰り返すマイクロチップという目に見えない世界では、たった一つの隠れたエラーがシステムの壊滅的な失敗を引き起こすことがあります。エンジニアは、データのストレージ要素間を時間が経過するにつれてどのように移動するかを記述する、RTL（レジスタ転送レベル）と呼ばれる言語を用いてこれらのチップを設計します。設計が製造される前に正しく動作することを保証するため、検証のエキスパートは「アサーション」を記述します。アサーションとは、設計自体に書き込まれた厳格なルール、つまり「もしこれが起きたら、次は必ずこうなるはずだ」という声明のようなものだと考えてください。もしチップがこのルールに違反した場合、システムはアラームを鳴らし、そうでなければ見過ごされてしまうであろうバグを明らかにします。数十年にわたり、これらのルールを書くことは、どの挙動が誤る可能性があるかをエンジニアが推測し、それに対して特定のチェックを記述する必要がある、遅くて手作業による、ミスが発生しやすい作業でした。コンピュータは既存の設計シミュレーションをマイニングしてパターンを見つけることで助けとなってきましたが、これらの自動化された手法は、依存しているランダムなテストがそのシナリオに決して遭遇しないという理由だけで、最も危険なシナリオを見逃してしまうことがよくあります。

香港科技大学（広州）の研究チームは、この問題を解決するための新しいアプローチを開発し、彼らのシステムをNeuroAssertionと呼んでいます。ランダムな偶然に頼ってバグを見つけるのではなく、彼らの手法はチップ設計における最も到達困難な挙動を能動的に探し出し、人工知能と形式論理を組み合わせて必要な安全ルールを記述します。プロセスは、どの部分がテストされているかをより容易に把握できるように設計を変換することから始まります。研究者たちは、特定の、引き起こすのが難しい条件がこれまでに発生したかどうかを追跡する特別なマーカーをコード内に挿入します。次に、モデルチェッカーとして知られる強力な数学的エンジンを使用して、設計にそれらの稀な条件を実行させるよう強制します。これにより、ランダムなシミュレーションでは永遠に見逃されるであろう挙動を露呈させる、極めて具体的なテストケースのセットが生成されます。これらの新しい、多様なトレースは、次のステップのためのより豊かな基盤を提供します。

システムがこれらの見つけにくい挙動を把握すると、生成フェーズへと移行します。システムは、観察されたデータに基づいて初期の安全ルールを作成するために、構文誘導合成（syntax-guided synthesis）と呼ばれる技術を使用します。しかし、研究者たちは、この最初のパスが完璧であることは稀であると認識していました。これを修正するために、彼らは厳格な編集者のように機能するリファインメント・ループ（洗練ループ）を導入しました。システムは、コードに「ミュータント」として知られる小さな意図的なエラーを注入することで、現在のルールセットが設計の変化をどの程度検出できるかを測定します。もしルールがミュータントを捉えられなかった場合、システムはどの挙動がチェックされていないかを正確に把握します。その後、大規模言語モデルを呼び出し、そのギャップを埋めるために特別に設計された新しいルールを提案させます。もし提案されたルールに論理的な欠陥がある場合、第二の言語モデルはそれを単に破棄するのではなく、そのエラーを分析し、ルールを修復するための指示、すなわち文法（グラマー）を構築して、シンボリックソルバーを導きます。これにより、アサーションが豊富かつ堅牢になるまで、提案、チェック、修正を行うサイクルが作成されます。

このアプローチの結果は、小規模な調停回路から複雑なプロセッサコアに至る7つの異なるチップ設計でテストされました。新しいフレームワークは、このリファインメントなしでの単一パスのマイニングに依存するSMARTとして知られる従来の最先端手法を一貫して上回りました。これらの実験において、NeuroAssertionは古い手法よりも約2倍多くのアサーションを生成しました。より重要なことに、これらのルールの品質は大幅に高かったのです。注入されたエラーを検出する能力によって測定すると、新しいシステムは伝統的なアプローチの約2倍のカバー率を達成しました。特定のベンチマークにおいては、その改善はさらに劇的であり、例えば、あるプロセッサコンポーネントでは、ミューテーション・カバレッジは約6パーセントから32パーセント以上に跳ね上がりました。研究者たちはまた、形式的なチェックやリファインメントのステップなしに、大規模言語モデルにルールを書かせる直接的なアプローチとも比較を行いました。その直接的な手法は、はるかに少ない数のルールしか生成できず、潜在的なエラーのほとんどを捉えることに失敗しており、生の言語生成だけではこの極めて重要なタスクには不十分であることを示しました。

アサーション生成を、一度限りのイベントではなく、探索と洗練の継続的なループとして扱うことで、研究者たちは、複雑なハードウェアに対して高品質な安全ルールを自動生成することが可能であることを示しました。このシステムは単に推測するのではなく、設計の死角を能動的に探し出し、ニューラルネットワークと形式論理のパートナーシップを利用してそれらを埋めます。この研究は、ハードウェア検証の未来が、人工知能のパターン認識と数学的証明の厳格な確実性を組み合わせることにあり、それによって私たちの世界を動かすチップが、それを設計するエンジニアと同様に信頼できるものであることを保証することを示唆しています。