RISC-V Formal Verification Framework (riscv-formal) についてまとめる (14. riscv-formalでCLZ命令を検証する)

riscv-formalフレームワークを使用してCLZ命令の動作を検証する。

riscv-formalでの検証設定

1. 検証用テストケースの作成

insns/insn_clz.vを作成して、CLZ命令の検証用テストケースを定義した：

module rvfi_insn_clz (
  input clock,
  input reset,
  `RVFI_INPUTS
);

`RVFI_WIRES

// CLZ命令の検証
wire [31:0] clz_rd = rvfi_rs1_rdata == 0 ? 32 : 31 - $clog2(rvfi_rs1_rdata | 1);

assign spec_valid = rvfi_valid && rvfi_insn[6:0] == 7'b0010011 &&
                    rvfi_insn[14:12] == 3'b001 && rvfi_insn[24:20] == 5'b00000 &&
                    rvfi_insn[31:25] == 7'b0110000;

assign spec_rs1_addr = rvfi_insn[19:15];
assign spec_rd_addr = rvfi_insn[11:7];
assign spec_rd_wdata = clz_rd;
assign spec_trap = 0;

`RVFI_ASSERT
endmodule

2. 検証設定ファイルの作成

cores/VexRiscv/checks/insn_clz_ch0.sbyを作成：

[options]
mode bmc
depth 20

[engines]
smtbmc boolector

[script]
read -formal cores/VexRiscv/VexRiscv.v
read -formal ../../insns/insn_clz.v
read -formal ../../checks/rvfi_insn_check.sv

[files]
cores/VexRiscv/VexRiscv.v
../../insns/insn_clz.v
../../checks/rvfi_insn_check.sv

検証実行と結果

実行コマンド

cd riscv-formal/cores/VexRiscv/checks
make insn_clz_ch0

実行結果

検証は成功し、以下の結果が得られた：

SBY 15:54:11 [insn_clz_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 15:54:11 [insn_clz_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 15:54:11 [insn_clz_ch0] engine_0: ##   0:00:00  Skipping step 1..
...
SBY 15:54:11 [insn_clz_ch0] engine_0: ##   0:00:00  PASSED
SBY 15:54:11 [insn_clz_ch0] engine_0: finished (returncode=0)
SBY 15:54:11 [insn_clz_ch0] engine_0: status returned by engine: PASS