現在開発中のハードウェア記述言語Verylではコンパイラ中に様々な式評価があります。
この式評価においては、例えば各ビットは0/1の2値ではなく0/1/x/zの4値だったり、変数のサイズは可変（1ビットから数千ビットまで）だったりと、単純な固定長整数型の四則演算に比べてかなり複雑です。
さらに、VerylはSystemVerilogの意味論を継承しているため、SystemVerilogの規格書（IEEE 1800-2023）に書かれた細かい式評価のルールにも準拠する必要があります。
また、Verylコンパイラが内蔵しているRTLシミュレータでは高速化のためにCraneliftのIRやCのソースコードを生成してネイティブ実行バイナリを得るパスを持っており、ここで生成するコードについても上記のルールをすべて満たす必要があります。
このように複雑な式評価のルールを単体テストだけですべて検証するのは難しく、これまでもしばしば評価結果の間違いが報告されていました。このような場合に（原理的には）形式検証の出番ということになります。
形式検証の問題の1つは証明を書くコストが高い、ということだと思いますが、現在ではそのコストをLLMに負わせることができます。今回は @mizchi さんのGist「実装コードから仕様を吸い出して Z3 / TLA+ でバグを払い出す — 実践プレイブック」を参考に検討を始めましたが、Verylコンパイラの事情に合わせていろいろ変えています。
まず元のGistでは検証対象のモデルをLLMが実装から抽出し、Z3/TLA+で検証する形になっています。これにより実装言語は何でも良くなり適用範囲が非常に広いですが、実装とモデルの解離は問題になります。
VerylはRust実装なのでRustコードを直接検証するためにKaniを使うことにしました。
また、Gistでは検証すべき意味論も実装から抽出しますが、Verylの意味論の一部はSystemVerilogの意味論そのものなのでIEEE 1800-2023の規格書を直接参照させました。SVと関係ないコンパイラの内部実装についてはGistと同じく実装からの抽出にしています。
実際に作業しているリポジトリが以下になります。
https://github.com/veryl-lang/formal
LLMとしてはCodexのSol 6.1を使い、Kaniの証明とKaniで証明しきれない部分のダイレクトテスト、ミューテーションテストを自動で生成させます。
完全自動だとKaniの証明をあきらめてダイレクトテストに逃げがちなので、なるべくKani側で証明しきれるように時々ヒントを与えています。
また、CIで毎晩最新のVerylに対して検証を実行し、エラーがあればIssue報告するので、これをCodexが修正する、というフローになります。
これまでに以下のようなバグを発見・修正しています。主に4値評価や符号拡張のコーナーケースですが、LSPにおける座標計算の間違いなども発見しています。
- Reject and repair corrupted cache blobs
- Correct source coordinates and LSP UTF-16 positions
- Preserve sequential state through synthesis
- Fix expression evaluation and selection geometry
- Fix simulator selections and four-state values
- Fix four-state expression semantics
- Fix synthesis cast boundaries and mixed signedness
また、SystemVerilogの規格書自体の曖昧性も発見しました。
不定を含む単項演算（例えば +2'b0x）は規格上以下の2つのルールがあります。
- 単項
+の結果はそのオペランドと等しい - 不定を含む算術演算の結果は全体を不定とする（単項
+に対する例外規定はなし）
1つ目のルールに従えば +2'b0x の結果は 2'b0x 、2つ目なら 2'bxx です。
これについては単項+は回路を生成しないので不定が全幅に伝搬する理由がないことと、
既存の実装（Icarus VerilogとSynopsys VCS）の挙動を参考に前者の解釈としました。
Verylコンパイラで運用している形式検証について紹介しました。特にRTLシミュレータにおいては高速化のために特定のビット幅専用の最適化パスなどを書くことが多いので、こういった形で検証範囲が拡大するのは非常に有用そうです。
Discussion
