FPGA開発日記

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

RISC-V Formal Verification Framework (riscv-formal) についてまとめる (3. 信号の定義)

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

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

yosyshq.readthedocs.io

前回の続き: msyksphinz.hatenablog.com

代替算術演算

算術演算のチェックにおいて、乗算や除算などの演算をハードウェアチェッカーで処理するのは、現代のハードウェアモデルチェッカーを用いても現実的ではない。

それでも、そうした演算を実行する算術ユニットのバイパスなどを検証できるようにするため、代替算術演算のセットを定義する。

RISCV_FORMAL_ALTOPS : riscv-formal はテスト対象のプロセッサが代わりにこれらの代替演算を実装することを期待している。

  • 可換演算(乗算など): 加算に続いて演算の種類を示すビットマスクとの排他的論理和に置き換えられる。
  • 非可換演算(除算など): 減算に続いて演算の種類を示すビットマスクとの排他的論理和に置き換えられる。

ビットマスクは64ビット幅である。RV32実装ではビットマスクの下位32ビットのみを使用する。RV64の*W命令（MULWなど）は、オペランドの下位32ビットを加算または減算し、ビットマスクの下位32ビットとXOR演算した後、結果を64ビットに符号拡張される。

整数乗算・除算命令

この表に基づくと、例えば A * B は (A + B) ^ 0x2cdf52a55876063e に置き換えられて出力されるべきである？

Operation Add/Sub Bitmask
MUL Add 0x2cdf52a55876063e
MULH Add 0x15d01651f6583fb7
MULHSU Sub 0xea3969edecfbe137
MULHU Add 0xd13db50d949ce5e8
DIV Sub 0x29bbf66f7f8529ec
DIVU Sub 0x8c629acb10e8fd70
REM Sub 0xf5b7d8538da68fa5
REMU Sub 0xbc4402413138d0e1

制御およびステータスレジスタ（CSR）

サポートされる各CSRには、各CSRについて4つのポートを定義する。

テスト対象コアが RVFI 経由でトレースする各 CSR に対して、Verilog 定数 RISCV_FORMAL_CSR_<CSRNAME> を設定しなければならない。

output [NRET * XLEN - 1 : 0] rvfi_csr_<csrname>_rmask
output [NRET * XLEN - 1 : 0] rvfi_csr_<csrname>_wmask
output [NRET * XLEN - 1 : 0] rvfi_csr_<csrname>_rdata
output [NRET * XLEN - 1 : 0] rvfi_csr_<csrname>_wdata
  • rmask/wmask (XLEN-bit): rdataとwdataのどのビットが有効かを指定する(1-bit単位でマスクする)
    • 命令が要求する以上のrmask/rdataビットを有効化することは問題ない。
    • ただし、報告されるビットがマシンの状態を正しく反映している場合に限る。
  • CSRの読み取りに副作用がある場合、その副作用はrmaskビットの有効化によって引き起こされてはならない。

投機的実行の処理

投機的に実行するアウト・オブ・オーダー・コアは、RVFI上命令を投機的にコミットできる。

この場合、ロールバックはロールバック・インターフェース経由で出力されねばならない。これはRISCV_FORMAL_ROLLBACKが定義された時に有効になる：

output [ 0 : 0] rvfi_rollback_valid
output [63 : 0] rvfi_rollback_order

rvfi_rollback_validがアサートされたサイクルより前に出力された、rvfi_orderフィールドがrvfi_rollback_order以上である全てのRVFIパケットは無効化される。

rvfi_rollback_validと同じサイクルに出力されたRVFIパケットは、rvfi_rollback_orderで示された命令番号からの再開される命令の一部なので、取り込む必要がある。

動的フォルトの処理

命令フェッチまたはデータアクセスのフォルトチェックが外部バスの応答によって決定されるコアは、RVFIを介してそのようなフォルトを通知できる(つまりPMAなどの設定以外に、バスの応答によってフォルトが発生する場合など)。

RISCV_FORMAL_MEM_FAULTが定義されている場合、RVFIインターフェースは次の信号によって拡張される：

output [NRET          - 1 : 0] rvfi_mem_fault
output [NRET * XLEN/8 - 1 : 0] rvfi_mem_fault_rmask
output [NRET * XLEN/8 - 1 : 0] rvfi_mem_fault_wmask
  • 命令フェッチにおいてフォルトが発生した場合、 rvfi_insn を全ゼロに設定し、rvfi_mem_fault を設定する。
  • メモリアクセスにおいてフォルトが発生した場合、rvfi_mem_fault を設定するが、レジスタやメモリへの書き込みは一切行わない。
    • 代わりに、アクセスがフォルトを起こさなかった場合にアクセスされるはずだったバイトが rvfi_mem_fault_rmask と rvfi_mem_fault_wmask に出力される。アドレスは依然として rvfi_mem_addr 経由で出力される。
      • NOTE: つまり、元のメモリの値を通知する必要がある、ということ？