https://msyksphinz.hatenablog.com/entry/2025/09/02/040000

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

下記の情報をもとに、どういう情報を接続させればよいのかチェックしていくことにする。

yosyshq.readthedocs.io

用語

XLEN : RISC-V ISA仕様書に記載されているxレジスタのビット幅
NRET : テスト対象コアが1サイクルでリタイアできる命令の最大数
ILEN : テスト対象プロセッサの最大命令幅 (通常は32)
リタイアされた複数の命令が同一レジスタを書き込む場合、インデックスが最も高いチャネルが競合に勝った命令を含む。

命令のメタデータ

output [NRET        - 1 : 0] rvfi_valid
output [NRET *   64 - 1 : 0] rvfi_order
output [NRET * ILEN - 1 : 0] rvfi_insn
output [NRET        - 1 : 0] rvfi_trap
output [NRET        - 1 : 0] rvfi_halt
output [NRET        - 1 : 0] rvfi_intr
output [NRET * 2    - 1 : 0] rvfi_mode
output [NRET * 2    - 1 : 0] rvfi_ixl

rvfi_valid (1-bit) : コアが命令をリタイアさせるときにアサートされる。
- 以下の信号は、 rvfi_valid がアサートされているときにのみ有効な信号である。
rvfi_order (64-bit) : 命令インデックス
- インデックスは重複使用してはならず、欠番があってはならない。因果関係が保たれる限り命令はリオーダリングされた形でリタイアされてもよい。
  - レジスタおよびメモリ書き込み操作は、それらに依存する読み出し操作の前にリタイアされなければならない
rvfi_insn (ILEN-bit) : 命令の命令ワード
- ILEN ビット未満の命令の場合、この出力の上位ビットは全てゼロでなければならない。
  - 圧縮命令の場合、圧縮された命令ワードをこのポートに出力しなければならない。
  - 融合命令の場合、完全な融合命令シーケンスを出力しなければならない。
    - Note: 融合命令がどういうのか分からないが、Fusionされた場合でも分解して出力しなければならない、ということ？
rvfi_trap: (1-bit) : デコードできない命令の出力時にアサートされる
- アライメント違反のメモリ読み書き
- その他のメモリアクセス違反
- アライメント違反命令へのジャンプ命令
rvfi_halt (1-bit) : 命令がコアが実行を停止する前にリタイアする最後の命令である場合に設定される。
- この信号は生存性プロパティの検証を可能にする
  - まだCPUが何かの命令を実行している最中であることを示す？
rvfi_intr (1-bit): トラップハンドラの先頭の命令時に設定される
- つまり、rvfi_pc_rdata が前の命令の rvfi_pc_wdata と一致しない命令である場合
rvfi_mode (2-bit): 現在の特権レベル
- 0=U-Mode、1=S-Mode、2=Reserved、3=M-Mode
rvfi_ixl (2-bit): 現在の特権レベルにおける MXL/SXL/UXL
- Machine Mode / Supervisor Mode / User Mode のXLEN
- 1=32、2=64

整数レジスタの読み書き

output [NRET *    5 - 1 : 0] rvfi_rs1_addr
output [NRET *    5 - 1 : 0] rvfi_rs2_addr
output [NRET * XLEN - 1 : 0] rvfi_rs1_rdata
output [NRET * XLEN - 1 : 0] rvfi_rs2_rdata

rvfi_rs1_addr / rvfi_rs2_addr (5-bit): 命令の rs1 および rs2 レジスタアドレス
- rs1/rs2 レジスタを読み込まない命令の場合はどのような値を設定してもよい。
- ただし、この出力がゼロでない場合、rvfi_rs1_rdata はそのレジスタの前のステートの値を出力しなければならない
rvfi_rs1_rdata/rvfi_rs2_rdata (XLEN-bit): 命令の実行前の rs1/rs2 でアドレス指定された x レジスタの値
- rs1/rs2 が 0 の場合、この出力は 0 でなければならない。

output [NRET *    5 - 1 : 0] rvfi_rd_addr
output [NRET * XLEN - 1 : 0] rvfi_rd_wdata

rvfi_rd_addr (5-bit): 命令のrdレジスタアドレス
- rdレジスタを書き込みしない命令の場合、常にゼロでなければならない。
rvfi_rd_wdata は、この命令実行後にrd が参照する x レジスタの値である。
- つまり、 rd に書き込む値である。
- rdが0の場合、この出力は 0 でなければならない。

プログラムカウンタ

output [NRET * XLEN - 1 : 0] rvfi_pc_rdata
output [NRET * XLEN - 1 : 0] rvfi_pc_wdata

rvfi_pc_rdata (XLEN-bit): 命令実行前のプログラムカウンタ
rvfi_pc_wdata (XLEN-bit): 命令実行後の次の命令のプログラム・カウンタ
rvfi_intr の制御時に使用する

メモリ・アクセス

output [NRET * XLEN   - 1 : 0] rvfi_mem_addr
output [NRET * XLEN/8 - 1 : 0] rvfi_mem_rmask
output [NRET * XLEN/8 - 1 : 0] rvfi_mem_wmask
output [NRET * XLEN   - 1 : 0] rvfi_mem_rdata
output [NRET * XLEN   - 1 : 0] rvfi_mem_wdata

rvfi_mem_rmask / rvfi_mem_wmask (XLEN/8-bit) : メモリ・オペレーションであることを示す
- これらのマスク値が0以外である場合
rvfi_mem_addr(XLEN-bit): アクセスされたメモリ・アドレス
RISCV_FORMAL_ALIGNED_MEM の defineにより、メモリアクセスのアライン判定を切り替える
- XLEN=32 では 4 バイトアラインメントでなければならない
- XLEN=64 では 8 バイトアラインメントでなければならない
- RISCV_FORMAL_ALIGNED_MEM が定義されていない場合、アドレスはアクセスされる LSB またはワード/ハーフワード/バイトを直接指さなければならない。
  - NOTE: どうやって？
rvfi_mem_rmask (XLEN/8-bit) : 読み込まれたデータの有効位置を示すマスク
- rvfi_mem_addr から読み込まれたデータrvfi_mem_rdata のうち有効なバイト位置を示す。
rvfi_mem_wmask (XLEN/8-bit): 書き込まれたデータの有効位置を示すマスク
- rvfi_mem_addr に書き込まれた有効なデータrvfi_mem_wdata のうち有効なバイト位置を示す。
rvfi_mem_rdata (XLEN-bit): rvfi_mem_addr から読み出されたデータ
- rvfi_mem_rmask により有効なバイト位置が指定される。
rvfi_mem_wdata (XLEN-bit): rvfi_mem_addr に書き込まれたデータ
- rvfi_mem_wmask は有効なバイトを指定する。

RISCV_FORMAL_ALIGNED_MEM が設定されている場合、riscv-formal はアラインメント違反のメモリアクセスがトラップを引き起こすと仮定している。