Btor2MLIR: A Format and Toolchain for Hardware Verification

あなたは、謎を解こうとしている探偵だと想像してください。しかし、手がかりは、限られた専門家にしか読めない秘密のコードで書かれています。コンピュータサイエンスの世界では、この「秘密のコード」とは、コンピュータチップ（ハードウェア）がどのように振る舞うべきかを記述するための言語です。エンジニアは、スマートフォンから宇宙船に至るまで、あらゆるものを動かすためのチップを構築しますが、設計にたとえ微細なミスがあっても、システム全体がクラッシュしたり、異常な動作をしたりすることがあります。これを防ぐために、研究者は「形式手法（formal methods）」を使用します。これは、設計が完璧であることを証明するための、スーパーパワーを備えたスペルチェッカーのような数学的ツールです。

長い間、これらのスペルチェッカーは異なる言語を話していました。あるものは、ハードウェア・コンペティションで人気のあるフォーマットである「BTOR2」を話し、別のものは、ソフトウェア・コンパイラがコードをチェックするために使用する「LLVM-IR」という言語を使用しています。それは、フランス語から英語への翻訳しかできない通訳者と、スペイン語から英語への翻訳しかできない通訳者がいるようなものでした。もしあなたが、スペイン語の本をチェックするためにフランス語の通訳者を使いたいと思っても、手が出ません。そのたびに、ゼロから新しい翻訳者を作り直す必要がありました。この論文は、BTOR2MLIRと呼ばれる、新しい魔法の翻訳者を紹介しています。これは中間地点に位置し、ハードウェア設計が、毎回車輪を再発明することなくソフトウェアツールと対話できるようにするための、ユニバーサルな架け橋として機能します。

問題点：多すぎる方言、足りない架け橋

ハードウェア検証の世界では、BTOR2フォーマットが、Hardware Model Checking Competition (HWMCC) のようなコンペティションのための回路記述の標準となっています。BTOR2を、デジタル回路がどのように数値をカウントし、加算し、あるいはエラーをチェックするかを記述するための、非常に具体的で効率的な「方言」だと考えてください。BTORMCのようなツールは、この方言を読み取り、回路が安全かどうかをチェックするために特別に構築されています。

しかし、ソフトウェア検証の世界は巨大で強力です。SEAHORNのようなツールは、LLVM-IRという言語で書かれたソフトウェアコードをチェックするエキスパートです。これらのツールは、LLVMコンパイラ・インフラストラクチャのような大規模なプロジェクトによって数十年にわたり洗練されており、非常に成熟しています。これらには、コードを最適化したり、バグを見つけたり、シミュレーションを実行したりするための組み込み機能があります。

問題は、これら二つの世界が滅多に会話しないことです。強力なソフトウェアツールを使用してハードウェア設計をチェックするために、研究者はカスタムの使い捨ての翻訳機を書かなければなりませんでした。それは、毎回正方形の杭を丸い穴に無理やり押し込もうとするようなものでした。これらの翻訳機は、ソフトウェアツールに既に存在する基本機能（数値やループの扱い方など）を再実装しなければならないことが多く、無駄な努力や潜在的なエラーにつながりました。

解決策：ユニバーサル・アダプター (BTOR2MLIR)

この論文の著者であるウォータールー大学のJoseph Tafese、Isabel Garcia-Contreras、およびArie Gurfinkelは、より優れた架け橋を作ることに決めました。彼らは、MLIR (Multi-Level Intermediate Representation) に基づく新しいフォーマットおよびツールチェーンであるBTOR2MLIRを作成しました。

MLIRを理解するために、巨大でモジュール式のレゴセットを想像してみてください。異なるタイプの家を建てるたびにゼロから城を作る代わりに、MLIRは、組み立てることができるベースとなるレゴのブロック（ダイアレクト）を提供します。BTOR2と全く同じように見え、かつ振る舞う新しい「ハードウェア」ブロックを定義でき、それを既存の「ソフトウェア」のレゴ構造に直接スナップさせることができます。

彼らの新しいツールの仕組みは以下の通りです：

1. 翻訳機（The Translator）: 彼らはMLIRの中に「BTORダイアレクト」を構築しました。これは、BTOR2フォーマットの直接的かつロスレスな翻訳です。BTOR2ファイルがあれば、BTOR2MLIRは即座にこのMLIRダイアレクトへと変換できます。
2. 架け橋（The Bridge）: MLIRは拡張性を備えて設計されているため、彼らは彼らのBTORダイアレクトを標準的なLLVMダイアレクトへと変換する「変換パス」を作成しました。これが魔法のステップです。ハードウェアの記述を取り込み、SEAHORNのようなソフトウェアツールがネイティブに理解できる形式へと変換します。
3. 結果（The Result）: 出力されるのはLLVM-IRであり、これはソフトウェア検証エンジンが取り込んで分析できる言語です。

実験：それは本当に機能するのか？

チームは単に架け橋を作っただけでなく、その上にトラックを走らせて、耐えられるかどうかを確認しました。彼らは、HWMCCコンペティション（具体的には2020年と2019年のセット）からの実世界のハードウェア・ベンチマークのコレクションを取り出し、新しいツールチェーンに通しました。

まず、正確性をチェックしました。彼らはBTOR2ファイルをとり、それをMLIRフォーマットに変換し、その後、再びBTートBTOR2へと変換しました。そして、元のファイルと、ラウンドトリップ（往復）させたファイルを比較しました。結果はどうだったでしょうか？それらは同一でした。安全性プロパティ（回路が従わなければならないルール）は完璧に保持されていました。元のツールがタイムアウトしたりメモリ不足になったりした難しいケースにおいても、彼らのラウンドトリップ版は問題を解決できる場合があり、これは翻訳がエラーを導入していないことを示唆しています。

次に、パフォーマンスをテストしました。彼らは、この新しい「ハイブリッド」パイプラインを、有名なソフトウェア・モデルチェッカーであるSEAHORNおよび高速ソルバーであるBOOLECTORに接続しました。そして、この新しいパイブリッド・パイプラインを、BTOR2専用に構築されたゴールドスタンダードのツールであるBTORMCと比較しました。

結果は驚くべきものであり、勇気づけられるものでした：

• 速度: 多くの場合、ハイブリッド・パイプライン（BTOR2MLIR + SEAHORN + BOOLECTOR）は、専用のBTORMCツールと同等の性能、あるいはそれよりも高速でした。例えば、「19/mann」カテゴリのベンチマークでは、ハイブリッド・アプローチは約3,190秒で44のインスタンスを解決しましたが、BTORMCはより多くのインスタンスで時間がかかるか、タイムアウトしました。
• 柔軟性: このツールは、除算やビットベクトルといった複雑な操作を正常に処理でき、MLIRの「レゴブロック」がハードウェア論理の重労働を扱えることを証明しました。
• 限界: 著者たちは、ツールがまだできないことについても正直に述べています。現在はビットベクトルと配列をサポートしていますが、「公平性（fairness）」や「正義（justice）」の制約（システムが無限の時間にわたってどのように振る舞うかに関するルール）はまだ扱えません。また、うまく機能してはいるものの、すべてのカテゴリにおいて専用のハードウェアツールを完全に圧倒したわけではなく、強力な競合相手ではあっても、完全な置き換えではありませんでした。

なぜこれが重要なのか

この論文は、ハードウェア検証のすべてを解決したと主張しているわけではありません。むしろ、新しい考え方を提案しています。ビデオゲームからウェブブラウザまであらゆるものを動かしているLLVMコンパイラの成熟した堅牢なインフラストラクチャを使用することで、ハードウェアの研究者は車輪の再発明をやめることができます。

著者たちは、ハードウェア設計を取り込み、それをユニバーサルな言語に翻訳し、既存の強力なソフトウェアツールを使用してそれをチェックできることを示しています。これは、迅速なプロトタイピングへの扉を開きます。もし研究者が新しい検証手法を試したいと思ったら、新しいエンジンを構築する必要はなく、単にそのアイデアをMLIRフレームワークにプラグインするだけでよいのです。

将来的には、チームはこの架け橋を、現在ソフトウェアで使用されているKLEE（シンボリック実行エンジン）やLIBFUZZER（ファジングツール）といった、さらに多くのツールに接続することを計画しています。これらはハードウェアのバグを見つける方法に革命をもたらす可能性があります。また、AIGERやSMT-LIBのような他のフォーマットの生成も計画しています。

究極的に、BTOR2MLIRは、ハードウェア検証とソフトウェア検証の間の壁が崩れつつあることの概念実証です。共通の言語を話すことで、私たちのデジタル世界をより安全に、より速く、そしてより簡単に構築できるようになることを示唆しています。