VexRiscv におけるriscv-formal の実行方法を調査している。
前回の続き： msyksphinz.hatenablog.com
insn_addi_ch0 にのみ注力して 動作を確認する
以下のコマンドで、insn_addi_ch0に注力して動作を確認する。
make -C checks insn_addi_ch0
make -C checks insn_addi_ch0 make: Entering directory '/home/msyksphinz/work/formal/riscv-formal/cores/VexRiscv/checks' sby insn_addi_ch0.sby SBY 15:54:09 [insn_addi_ch0] Writing '/home/msyksphinz/work/formal/riscv-formal/cores/VexRiscv/checks/insn_addi_ch0/src/defines.sv'. SBY 15:54:09 [insn_addi_ch0] Writing '/home/msyksphinz/work/formal/riscv-formal/cores/VexRiscv/checks/insn_addi_ch0/src/insn_addi_ch0.sv'. SBY 15:54:09 [insn_addi_ch0] Copy '/home/msyksphinz/work/formal/riscv-formal/cores/VexRiscv/../../checks/rvfi_macros.vh' to '/home/msyksphinz/work/formal/riscv-formal/cores/VexRiscv/checks/insn_addi_ch0/src/rvfi_macros.vh'. SBY 15:54:09 [insn_addi_ch0] Copy '/home/msyksphinz/work/formal/riscv-formal/cores/VexRiscv/../../checks/rvfi_channel.sv' to '/home/msyksphinz/work/formal/riscv-formal/cores/VexRiscv/checks/insn_addi_ch0/src/rvfi_channel.sv'. SBY 15:54:09 [insn_addi_ch0] Copy '/home/msyksphinz/work/formal/riscv-formal/cores/VexRiscv/../../checks/rvfi_testbench.sv' to '/home/msyksphinz/work/formal/riscv-formal/cores/VexRiscv/checks/insn_addi_ch0/src/rvfi_testbench.sv'. SBY 15:54:09 [insn_addi_ch0] Copy '/home/msyksphinz/work/formal/riscv-formal/cores/VexRiscv/../../checks/rvfi_insn_check.sv' to '/home/msyksphinz/work/formal/riscv-formal/cores/VexRiscv/checks/insn_addi_ch0/src/rvfi_insn_check.sv'. SBY 15:54:09 [insn_addi_ch0] Copy '/home/msyksphinz/work/formal/riscv-formal/cores/VexRiscv/../../insns/insn_addi.v' to '/home/msyksphinz/work/formal/riscv-formal/cores/VexRiscv/checks/insn_addi_ch0/src/insn_addi.v'. SBY 15:54:10 [insn_addi_ch0] engine_0: smtbmc boolector SBY 15:54:10 [insn_addi_ch0] base: starting process "cd insn_addi_ch0/src; yosys -ql ../model/design.log ../model/design.ys" SBY 15:54:10 [insn_addi_ch0] base: finished (returncode=0) SBY 15:54:10 [insn_addi_ch0] prep: starting process "cd insn_addi_ch0/model; yosys -ql design_prep.log design_prep.ys" SBY 15:54:10 [insn_addi_ch0] prep: finished (returncode=0) SBY 15:54:10 [insn_addi_ch0] smt2: starting process "cd insn_addi_ch0/model; yosys -ql design_smt2.log design_smt2.ys" SBY 15:54:10 [insn_addi_ch0] smt2: finished (returncode=0) SBY 15:54:10 [insn_addi_ch0] engine_0: starting process "cd insn_addi_ch0; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 20:21 --append 0 --dump-vcd engine_0/trace.vcd --dump-yw engine_0/trace.yw --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2" SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Solver: boolector SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 0.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 1.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 2.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 3.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 4.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 5.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 6.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 7.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 8.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 9.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 10.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 11.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 12.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 13.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 14.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 15.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 16.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 17.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 18.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 19.. SBY 15:54:11 [insn_addi_ch0] engine_0: ## 0:00:00 Checking assumptions in step 20.. SBY 15:54:14 [insn_addi_ch0] engine_0: ## 0:00:03 Checking assertions in step 20.. SBY 15:55:14 [insn_addi_ch0] engine_0: ## 0:01:03 waiting for solver (1 minute) SBY 15:59:14 [insn_addi_ch0] engine_0: ## 0:05:03 waiting for solver (5 minutes) SBY 16:03:40 [insn_addi_ch0] engine_0: ## 0:09:29 Status: passed SBY 16:03:40 [insn_addi_ch0] engine_0: finished (returncode=0) SBY 16:03:40 [insn_addi_ch0] engine_0: Status returned by engine: pass SBY 16:03:40 [insn_addi_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:09:30 (570) SBY 16:03:40 [insn_addi_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:09:30 (570) SBY 16:03:40 [insn_addi_ch0] summary: engine_0 (smtbmc boolector) returned pass SBY 16:03:40 [insn_addi_ch0] summary: engine_0 did not produce any traces SBY 16:03:40 [insn_addi_ch0] DONE (PASS, rc=0)
とりあえず走り始めたな。数分走った後、最終的にPASSまでやってきた。とりあえず動作をしているようだ。これはデザインを変えてみたらちゃんと検出できるかな？
diff --git a/cores/VexRiscv/VexRiscv.v b/cores/VexRiscv/VexRiscv.v index 2c3e57a..7c1e664 100644 --- a/cores/VexRiscv/VexRiscv.v +++ b/cores/VexRiscv/VexRiscv.v @@ -1066,7 +1066,7 @@ module VexRiscv ( assign _zz__zz_decode_SRC1_1 = (decode_IS_RVC ? 3'b010 : 3'b100); assign _zz__zz_decode_SRC1_1_1 = decode_INSTRUCTION[19 : 15]; assign _zz__zz_decode_SRC2_4 = {decode_INSTRUCTION[31 : 25],decode_INSTRUCTION[11 : 7]}; - assign _zz_execute_SrcPlugin_addSub = ($signed(_zz_execute_SrcPlugin_addSub_1) + $signed(_zz_execute_SrcPlugin_addSub_4)); + assign _zz_execute_SrcPlugin_addSub = ($signed(_zz_execute_SrcPlugin_addSub_1) + $signed(_zz_execute_SrcPlugin_addSub_4)) -1; assign _zz_execute_SrcPlugin_addSub_1 = ($signed(_zz_execute_SrcPlugin_addSub_2) + $signed(_zz_execute_SrcPlugin_addSub_3)); assign _zz_execute_SrcPlugin_addSub_2 = execute_SRC1; assign _zz_execute_SrcPlugin_addSub_3 = (execute_SRC_USE_SUB_LESS ? (~ execute_SRC2) : execute_SRC2);
一応、ちゃんと検出できたようだ。
SBY 16:10:46 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 14.. SBY 16:10:46 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 15.. SBY 16:10:46 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 16.. SBY 16:10:46 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 17.. SBY 16:10:46 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 18.. SBY 16:10:46 [insn_addi_ch0] engine_0: ## 0:00:00 Skipping step 19.. SBY 16:10:46 [insn_addi_ch0] engine_0: ## 0:00:00 Checking assumptions in step 20.. SBY 16:10:48 [insn_addi_ch0] engine_0: ## 0:00:02 Checking assertions in step 20.. SBY 16:10:54 [insn_addi_ch0] engine_0: ## 0:00:08 BMC failed! SBY 16:10:54 [insn_addi_ch0] engine_0: ## 0:00:08 Assert failed in rvfi_testbench: rvfi_insn_check.sv:177.7-177.40 (_witness_.check_flatten_checker_inst__assert_rvfi_insn_check_sv_177_86) SBY 16:10:54 [insn_addi_ch0] engine_0: ## 0:00:08 Writing trace to VCD file: engine_0/trace.vcd SBY 16:10:55 [insn_addi_ch0] engine_0: ## 0:00:09 Writing trace to Verilog testbench: engine_0/trace_tb.v SBY 16:10:56 [insn_addi_ch0] engine_0: ## 0:00:09 Writing trace to constraints file: engine_0/trace.smtc SBY 16:10:56 [insn_addi_ch0] engine_0: ## 0:00:09 Writing trace to Yosys witness file: engine_0/trace.yw SBY 16:10:56 [insn_addi_ch0] engine_0: ## 0:00:10 Status: failed SBY 16:10:56 [insn_addi_ch0] engine_0: finished (returncode=1) SBY 16:10:56 [insn_addi_ch0] engine_0: Status returned by engine: FAIL SBY 16:10:56 [insn_addi_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:11 (11) SBY 16:10:56 [insn_addi_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:11 (11) SBY 16:10:56 [insn_addi_ch0] summary: engine_0 (smtbmc boolector) returned FAIL SBY 16:10:56 [insn_addi_ch0] summary: counterexample trace: insn_addi_ch0/engine_0/trace.vcd SBY 16:10:56 [insn_addi_ch0] summary: failed assertion rvfi_testbench._witness_.check_flatten_checker_inst__assert_rvfi_insn_check_sv_177_86 at rvfi_insn_check.sv:177.7-177.40 step 20 SBY 16:10:56 [insn_addi_ch0] DONE (FAIL, rc=0)
波形を確認する。問題となる部分を検出できた。
