FormalRTL: Verified RTL Synthesis at Scale

この論文は、曖昧な仕様や形式保証の欠如といった産業規模のハードウェア設計における課題を克服するため、ソフトウェア参照モデルを形式仕様として統合し、計画・合成・形式等価性検査を密接に連携させる新しいマルチエージェントフレームワーク「FormalRTL」を提案し、大規模な産業グレードのベンチマークによる評価でその有効性を示したものです。

要約

🏗️ 背景：なぜこれが難しいのか？

今、AI の性能が向上するにつれて、GPU や NPU といった「計算を専門にするチップ」の設計が非常に難しくなっています。
これまでの AI（大規模言語モデル）は、文章からコードを書くのが得意ですが、**「自然言語（英語や日本語）だけで、複雑な電子回路の設計図（RTL コード）を完璧に作るのは、まだ無理がある」**というのが現状です。

• 問題点 1： 指示が曖昧。「もっと速くして」と言われても、具体的にどう回路を組めばいいか AI は迷います。
• 問題点 2： 複雑すぎる計算。普通の足し算ならいいですが、AI 向けの特殊な小数計算などは、シミュレーション（試運転）だけでは「ある特定の状況でバグが出る」という見落としが起きがちです。

💡 解決策：FormalRTL（フォーマル RTL）の登場

この論文では、**「AI に設計図を書かせる前に、まず『正解のモデル』を用意する」**という新しいアプローチをとっています。

🍳 料理の例えで説明します

1. 従来のやり方（失敗しやすい）：

   • 料理長（AI）に「美味しいカレーを作って」とだけ言います。
   • 料理長は「たぶんこうだろう」と適当に作ります。
   • 味見（シミュレーション）をしますが、たまたま美味しい時もあり、まずい時もあります。「本当に完璧な味か？」は保証されません。

2. FormalRTL のやり方（成功する）：

   • まず、プロの料理人が書いた**「完璧なレシピと味付けの基準（C 言語の参考モデル）」**を用意します。
   • AI（料理長）には、「この基準レシピを見ながら、同じ味のカレーを作ってください」と指示します。
   • AI が作ったカレーを、**「基準レシピ」と「AI のカレー」を同時に食べ比べる機械（形式検証ツール）**に入れます。
   • もし味が少しでも違えば、機械は**「ここが塩味が足りない（エラー）」**と具体的に教えてくれます。
   • AI はその指摘を受けて修正し、**「完全に味が一致するまで」**作り直します。

🤖 システムの仕組み：3 人の AI チーム

FormalRTL は、1 人の AI が全部やるのではなく、3 人の専門家がチームを組んで働きます。

1. 計画担当（Planning Agent）：

   • 役割： 大きな仕事を細分化する「プロジェクトマネージャー」。
   • 動き： 参考レシピ（C コード）を解析して、「まずは玉ねぎを切る部分から作りましょう」「次にスパイスを混ぜる部分」と、小さなタスクに分解します。
   • メリット： 一度に全部作ろうとすると AI は混乱しますが、小さく分ければ確実に作れます。

2. 作成担当（Initializing Agent）：

   • 役割： 実際に設計図を書く「職人」。
   • 動き： 分解された小さなタスクごとに、回路の設計図（RTL コード）を書きます。同時に、先ほどの「味見機械」が使えるようにする準備もします。

3. 修正担当（Debugging Agent）：

   • 役割： 間違いを直す「検査員兼リカバリーチーム」。
   • 動き： 味見機械（形式検証ツール）から「ここが間違っている」という**具体的なエラー報告（カウンター例）**を受け取ります。
   • すごいところ： 単に「バグあり」ではなく、「12 行目の計算式が間違っている」とピンポイントで指摘してくれるため、AI はすぐに修正できます。

📊 結果：どれくらいすごいのか？

研究者たちは、このシステムを使って、1000 行を超える複雑な回路の設計を AI にやらせました。

• 初回成功率： 最初は半分くらいしか成功しませんでしたが、修正を繰り返すことで、ほぼ 100% 成功させました。
• 規模： 従来の AI 研究では「足し算回路」程度しか作れませんでしたが、今回は**「産業レベルの複雑な計算回路」**も作れることを証明しました。
• 品質： 人間が手作業で設計したものと比べると、少し面積や速度は劣るものの、**「絶対に間違っていない（正解である）」**という点が最大の特徴です。

🚀 まとめ：なぜこれが重要なのか？

これまでの AI は「なんとなくコードを書く」のが得意でしたが、FormalRTL は**「正解の基準を持って、間違いを数学的に証明しながら作る」**ことに成功しました。

これは、**「AI が作った半導体が、実際にスマホや AI チップに入っても、絶対にバグで壊れない」**という信頼性を初めて保証する一歩です。今後は、この技術を使って、より複雑で高性能なチップを、人間が手作業で設計するよりもはるかに早く、安全に作れるようになるでしょう。

一言で言えば：

「AI に設計図を書かせる際、『正解のレシピ』と『自動検査機』をセットにして、間違いをゼロにするシステムを作りました」

技術概要

FormalRTL: Verified RTL Synthesis at Scale 技術的サマリー

本論文は、大規模言語モデル（LLM）を用いたハードウェア合成の課題を解決し、産業レベルの複雑な設計に対して形式的な正しさを保証するエンドツーエンドのマルチエージェントフレームワーク「FormalRTL」を提案するものです。

以下に、問題定義、手法、主要な貢献、実験結果、および意義について詳細にまとめます。

1. 問題定義

近年、LLM は自然言語理解やコード生成において優れた能力を示していますが、産業規模のデータパス中心のハードウェア設計（RTL 合成）への適用には以下の 2 つの根本的な課題が存在します。

1. 大規模設計の複雑さ: 産業用 IP コアは数千行の RTL コードを必要とします。従来の自然言語仕様のみに基づくアプローチでは、仕様の曖昧さや LLM のアーキテクチャ判断能力の限界により、大規模な設計を適切に分解・計画することが困難です。
2. 複雑な演算・論理構造: 産業用設計は、深いネストされたデータパスや独自データ型（bfloat16 や hifloat8 など）を含みます。従来のシミュレーションベースの検証では、コーナーケースの網羅が不十分であり、機能的な正しさを形式的に保証できません。

既存の LLM 駆動アプローチは、自然言語からの直接合成に依存しており、形式的な正しさを保証する「ソフトウェア参照モデル（C/C++ 等）」を有効活用できていませんでした。

2. 提案手法：FormalRTL

FormalRTL は、ソフトウェア参照モデル（C/C++）を形式的な実行可能仕様として活用し、計画、合成、検証、デバッグを密接に連携させるマルチエージェントパイプラインです。

主要な構成要素とフロー

1. 計画エージェント (Planning Agent):
   • C 参照モデルに対して静的解析（C コンパイラの AST 解析）を行い、設計を機能的なサブタスクに分解します。
   • 自然言語の仕様だけでなく、C コードの依存関係に基づいてモジュールを分割することで、アーキテクチャ的な曖昧さを排除し、ボトムアップ型の検証を可能にします。
2. 初期化エージェント (Initializing Agent):
   • 各サブモジュールに対して、C 参照モデルと仕様に基づき、初期 RTL コードと検証用ハーネス（テストベンチ）を生成します。
   • ハーネスは、C モデルと RTL モデルの入力を同一とし、出力の等価性をアサーションすることで、形式的検証の環境を構築します。
   • 順序回路（Sequential Logic）の場合、必要なクロックサイクル数を明示的にエンコードし、トランザクション等価性チェックを可能にします。
3. デバッグエージェント (Debugging Agent):
   • 等価性チェック（EC）ツール（hw-cbmc）からのフィードバック（構文エラーとカウンターエグザンプル）を用いて自動修正を行います。
   • バグロケーター: 構文エラーの位置を特定し、関連するコード行を抽出して LLM に提示します。
   • カウンターエグザンプル簡略化ツール: 複雑な検証レポートから、問題のある関数と不一致信号のみを抽出し、LLM が論理ミスの原因を迅速に特定できるようにします。
   • LLM はこれらの情報を基にパッチを生成し、コードを修正します。

特徴

• 形式的等価性チェック (Formal EC): ソフトウェアモデルとハードウェアモデルの間で数学的に等価性を証明し、シミュレーションの網羅性不足を克服します。
• ボトムアップ検証: 依存関係のある下位モジュールを先に検証・確定させるため、上位モジュールの生成時のデバッグ負荷を軽減します。

3. 主要な貢献

1. ソフトウェア参照モデル駆動の開発手法の確立: 静的解析と等価性チェックを用いて、スケーラビリティと正しさを保証する新しいアジャイルハードウェア開発手法を提案しました。
2. エンドツーエンドのマルチエージェントエンジン: 計画、合成、デバッグ、形式的検証までを自動化するパイプラインを実装しました。
3. 産業グレードベンチマークの構築と公開: 学術的および産業的シナリオ（FP16 演算子、Hifloat8 演算など）に基づき、仕様と C 参照モデルを備えた新しいベンチマークスイートを構築・公開しました。

4. 実験結果

新しいベンチマーク（1000 行を超える RTL 生成タスクを含む）を用いた評価結果は以下の通りです。

• 成功率: 多くの複雑なモジュールにおいて、初期生成での成功率（ISR）は低いものの、デバッグエージェントによる反復修正を経て、最終成功率（FSR）は 95%〜100% に達しました（一部の順序回路を除く）。
• 計画手法の比較: 自然言語仕様のみに依存するベースラインと比較し、FormalRTL は設計規模が大きくなるにつれて成功率を維持し、反復回数を効率的に抑えました。特に大規模設計（Design 4）では、ベースラインは 0% の成功率でしたが、FormalRTL は 100% を達成しました。
• デバッグツールの有効性: バグロケーターやカウンターエグザンプル簡略化ツールを除去したアブレーション実験では、修正回数が増加し、成功率が低下しました（特にカウンターエグザメントガイドなしでは 55% まで低下）。
• 品質 (QoR): 生成された RTL は、手動で最適化された設計と比較して面積や遅延において劣る傾向がありますが、機能的な正しさが保証された「実行可能なベースライン」として、エンジニアによるその後の PPA 最適化の基盤として極めて有用であることが示されました。

5. 意義と将来展望

FormalRTL は、LLM を用いたハードウェア合成において、「産業レベルの複雑さ」と「形式的な正しさの保証」という 2 つの大きな障壁を同時に克服した画期的なアプローチです。

• 産業への応用: 従来のプロトタイプ段階から、実際のチップ開発プロセスに LLM を統合する道を開きました。
• 開発効率化: 手動でのテストベンチ作成やデバッグの工数を大幅に削減し、アジャイルなハードウェア開発を可能にします。
• 今後の課題: 大規模な産業設計全体へのスケーラビリティ、カウンターエグザメント処理に特化した小型 LLM の開発、および C-RTL 等価性チェックツールのオープンソース化の促進が今後の課題として挙げられています。

本論文は、LLM によるハードウェア設計の信頼性を高め、実用化に向けた重要な一歩を示すものと言えます。