乗算器をSymbiYosysでフォーマル検証する戦略を考えている。
段階的Assertion戦略
8つの段階的チェック
64ビットの結果を8ビットずつ8段階に分けて検証する戦略を採用した：
`ifdef CHECK_8 assert (resp_result[ 7: 0] == model_result[ 7: 0]); `endif // CHECK_8 `ifdef CHECK_16 assume (resp_result[ 7: 0] == model_result[ 7: 0]); assert (resp_result[15: 8] == model_result[15: 8]); `endif // CHECK_16 `ifdef CHECK_24 assume (resp_result[15: 0] == model_result[15: 0]); assert (resp_result[23:16] == model_result[23:16]); `endif // CHECK_24 `ifdef CHECK_32 assume (resp_result[23: 0] == model_result[23: 0]); assert (resp_result[31:24] == model_result[31:24]); `endif // CHECK_32 `ifdef CHECK_40 assume (resp_result[31: 0] == model_result[31: 0]); assert (resp_result[39:32] == model_result[39:32]); `endif // CHECK_40 `ifdef CHECK_48 assume (resp_result[39: 0] == model_result[39: 0]); assert (resp_result[47:40] == model_result[47:40]); `endif // CHECK_48 `ifdef CHECK_56 assume (resp_result[47: 0] == model_result[47: 0]); assert (resp_result[55:48] == model_result[55:48]); `endif // CHECK_56 `ifdef CHECK_64 assume (resp_result[55: 0] == model_result[55: 0]); assert (resp_result[63:56] == model_result[63:56]); `endif // CHECK_64
8個のフォーマルを同時に動かして、チェックしてみることにした。
make bmc -j8 sby -f booth_mult_bmc.sby check_8 > booth_mult_bmc_check_8.log sby -f booth_mult_bmc.sby check_16 > booth_mult_bmc_check_16.log sby -f booth_mult_bmc.sby check_24 > booth_mult_bmc_check_24.log sby -f booth_mult_bmc.sby check_32 > booth_mult_bmc_check_32.log sby -f booth_mult_bmc.sby check_40 > booth_mult_bmc_check_40.log sby -f booth_mult_bmc.sby check_48 > booth_mult_bmc_check_48.log sby -f booth_mult_bmc.sby check_56 > booth_mult_bmc_check_56.log sby -f booth_mult_bmc.sby check_64 > booth_mult_bmc_check_64.log
最初の8ビットは検証できたが、次が検証できないな。
booth_mult_bmc_check_8.log
SBY 14:47:58 [booth_mult_bmc_check_8] engine_0: ## 0:07:16 Checking assumptions in step 63.. SBY 14:48:01 [booth_mult_bmc_check_8] engine_0: ## 0:07:20 Checking assertions in step 63.. SBY 14:48:05 [booth_mult_bmc_check_8] engine_0: ## 0:07:23 Status: passed SBY 14:48:05 [booth_mult_bmc_check_8] engine_0: finished (returncode=0) SBY 14:48:05 [booth_mult_bmc_check_8] engine_0: Status returned by engine: pass SBY 14:48:05 [booth_mult_bmc_check_8] summary: Elapsed clock time [H:MM:SS (secs)]: 0:07:24 (444) SBY 14:48:05 [booth_mult_bmc_check_8] summary: Elapsed process time [H:MM:SS (secs)]: 0:07:24 (444) SBY 14:48:05 [booth_mult_bmc_check_8] summary: engine_0 (smtbmc boolector) returned pass SBY 14:48:05 [booth_mult_bmc_check_8] summary: engine_0 did not produce any traces SBY 14:48:05 [booth_mult_bmc_check_8] DONE (PASS, rc=0)
booth_mult_bmc_check_16.log
SBY 14:40:41 [booth_mult_bmc_check_16] engine_0: ## 0:00:00 Solver: boolector SBY 14:40:41 [booth_mult_bmc_check_16] engine_0: ## 0:00:00 Checking assumptions in step 0.. SBY 14:40:41 [booth_mult_bmc_check_16] engine_0: ## 0:00:00 Checking assertions in step 0.. SBY 14:41:41 [booth_mult_bmc_check_16] engine_0: ## 0:01:00 waiting for solver (1 minute) SBY 14:45:41 [booth_mult_bmc_check_16] engine_0: ## 0:05:00 waiting for solver (5 minutes) SBY 14:50:41 [booth_mult_bmc_check_16] engine_0: ## 0:10:00 waiting for solver (10 minutes) SBY 14:55:41 [booth_mult_bmc_check_16] engine_0: ## 0:15:00 waiting for solver (15 minutes) SBY 15:10:41 [booth_mult_bmc_check_16] engine_0: ## 0:30:00 waiting for solver (30 minutes) SBY 15:40:41 [booth_mult_bmc_check_16] engine_0: ## 1:00:00 waiting for solver (1 hour) SBY 16:40:41 [booth_mult_bmc_check_16] engine_0: ## 2:00:00 waiting for solver (2 hours)
