RISC-V Formal Verification Framework (riscv-formal) についてまとめる

RISC-V Formal Verification Frameworkは、RISC-Vプロセッサの形式的検証を行うための包括的なフレームワークである。このフレームワークは、RISC-V Formal Interface (RVFI)を中心として構築されており、SystemVerilog Assertions (SVA)を活用した形式的テストベンチを提供する。

riscv-formalの目的と意義

riscv-formalの主な目的は、RISC-Vプロセッサの機能的正確性を数学的に証明することである。

従来のシミュレーションベースの検証では、テストケースの網羅性に依存するため、バグの見落としが発生する可能性がある。一方、形式的検証では、全ての可能な入力と状態遷移を数学的に検証することで、プロセッサの正確性を保証できる。

RISC-V Formal Interface (RVFI) の概要

RVFIは、riscv-formalフレームワークの中核となるインターフェースである。このインターフェースにより、RISC-Vコアの実行状態を外部の検証コンポーネントに伝達できる。

RVFIの主要信号

RVFIインターフェースは以下の主要な信号を定義している：

// 基本情報
input  [64:0] rvfi_valid,      // 有効なリタイア命令
input  [63:0] rvfi_order,      // 命令の実行順序
input  [31:0] rvfi_insn,       // 実行された命令
input  [63:0] rvfi_pc_rdata,   // プログラムカウンタ値
input  [63:0] rvfi_pc_wdata,   // 次のプログラムカウンタ値

// レジスタアクセス
input  [4:0]  rvfi_rs1_addr,   // ソースレジスタ1のアドレス
input  [4:0]  rvfi_rs2_addr,   // ソースレジスタ2のアドレス
input  [63:0] rvfi_rs1_rdata,  // ソースレジスタ1の読み取り値
input  [63:0] rvfi_rs2_rdata,  // ソースレジスタ2の読み取り値
input  [4:0]  rvfi_rd_addr,    // デスティネーションレジスタのアドレス
input  [63:0] rvfi_rd_wdata,   // デスティネーションレジスタの書き込み値

// メモリアクセス
input  [63:0] rvfi_mem_addr,   // メモリアドレス
input  [7:0]  rvfi_mem_rmask,  // 読み取りマスク
input  [7:0]  rvfi_mem_wmask,  // 書き込みマスク
input  [63:0] rvfi_mem_rdata,  // メモリ読み取りデータ
input  [63:0] rvfi_mem_wdata,  // メモリ書き込みデータ

// 制御状態
input  [63:0] rvfi_csr_mcycle_rdata,    // サイクルカウンタ
input  [63:0] rvfi_csr_mcycle_rmask,    // サイクルカウンタマスク
input  [63:0] rvfi_csr_mcycle_wdata,    // サイクルカウンタ書き込み値
input  [63:0] rvfi_csr_mcycle_wmask,    // サイクルカウンタ書き込みマスク

RVFIの特徴

非侵入性: プロセッサの内部実装に影響を与えない
標準化: 異なるRISC-V実装間で統一されたインターフェース
包括性: 命令実行、レジスタアクセス、メモリアクセス、CSR操作を全てカバー
拡張性: 新しい命令や機能の追加に対応

riscv-formalの検証手法

riscv-formalは、以下の複数の検証手法を組み合わせて使用する：

1. 形式的モデルチェッキング

SystemVerilog Assertions (SVA)を使用して、プロセッサの動作を数学的に検証する。

// 例：レジスタ書き込みの整合性チェック
property reg_write_consistency;
  @(posedge clk) disable iff (rst)
  rvfi_valid && rvfi_rd_addr != 0 |-> 
    rvfi_rd_wdata == expected_rd_value;
endproperty

assert property (reg_write_consistency);

2. 自動テスト生成

Pythonスクリプトを使用して、SBY (SymbiYosys)用のテストケースを自動生成する。

# テスト生成の例
def generate_arithmetic_tests():
    for op in ['add', 'sub', 'and', 'or', 'xor']:
        for rs1_val in range(-10, 11):
            for rs2_val in range(-10, 11):
                yield {
                    'instruction': f'{op} x3, x1, x2',
                    'rs1_value': rs1_val,
                    'rs2_value': rs2_val,
                    'expected_result': calculate_expected(op, rs1_val, rs2_val)
                }

3. リファレンスモデル比較

RISC-Vのリファレンス実装と比較して、動作の正確性を検証する。

riscv-formalで検出されるバグの例

riscv-formalは、従来のシミュレーションベース検証では発見困難なバグを検出できる：

1. 命令セマンティクスの問題

分岐予測の誤り: 条件分岐の予測ミスによる誤った実行パス
投機実行の問題: 投機的に実行された命令の副作用
例外処理の不備: 例外発生時の状態復旧の不完全性

2. バイパスとフォワーディングの問題

データハザード: レジスタの依存関係の処理ミス
フォワーディングパスの誤り: 最新の値を正しく伝達できない
ストール条件の不備: 必要な場合にパイプラインを停止しない

3. リセット処理の問題

不完全なリセット: 一部のレジスタがリセットされない
リセット順序の誤り: 依存関係のあるレジスタのリセット順序が不適切

4. 特殊なケース

コーナーケース: 極端な値や特殊な組み合わせでの動作異常
タイミング問題: クロックエッジでの状態遷移の不整合

riscv-formalの使用例

基本的な使用方法

１. RVFIインターフェースの実装

   // プロセッサにRVFI信号を追加
   output [64:0] rvfi_valid,
   output [31:0] rvfi_insn,
   // ... その他のRVFI信号

２. テストベンチの設定

   // riscv-formalのテストベンチをインスタンス化
   riscv_formal_monitor monitor (
       .clk(clk),
       .rst(rst),
       .rvfi_valid(rvfi_valid),
       .rvfi_insn(rvfi_insn),
       // ... その他の接続
   );

３. SBY設定ファイルの作成

   [tasks]
   cover
   prove
   
   [script]
   read_verilog -formal rvfi_interface.vh
   read_verilog processor.v
   read_verilog -formal testbench.v
   
   prep -top testbench
   
   [task cover]
   cover -stmts
   
   [task prove]
   prove -all

高度な使用方法

１. カスタムアサーションの追加

   // プロセッサ固有の検証ルール
   property custom_pipeline_check;
     @(posedge clk) disable iff (rst)
     rvfi_valid && is_load_instruction(rvfi_insn) |-> 
       ##[1:3] rvfi_valid && is_store_instruction(rvfi_insn);
   endproperty

２. CSR検証の実装

   // CSRの読み書き整合性チェック
   property csr_consistency;
     @(posedge clk) disable iff (rst)
     rvfi_valid && rvfi_csr_mcycle_rmask != 0 |-> 
       rvfi_csr_mcycle_rdata == expected_cycle_count;
   endproperty

次は、実際にチュートリアルを動かして動作を確認していきたい。

FPGA開発日記

カテゴリ別記事インデックス https://msyksphinz.github.io/github_pages , English Version https://fpgadevdiary.hatenadiary.com/