カテゴリインデックス：https://msyksphinz.hatenablog.com/entry/2024/12/14/040000
SymbiYosysを使った乗算器の形式検証
乗算器の検証の続き。
デザインの修正
デザインを修正した。修正後のコードは以下の通りである。
module mult ( input logic [ 7: 0] a, input logic [ 7: 0] b, output logic [15: 0] m ); logic [15: 0] tmp_m[9]; always_comb begin if (b[0]) begin tmp_m[0] = a; end else begin tmp_m[0] = 'h0; end for (int i = 1; i < 8; i++) begin if (b[i]) begin tmp_m[i] = tmp_m[i-1] + (a << i); end else begin tmp_m[i] = tmp_m[i-1]; end end end assign m = tmp_m[7]; `ifdef FORMAL always_comb begin assert (m == a * b); end `endif // FORMAL endmodule // mult
主な修正点は以下の通りである：
- 最初のビット（b[0]）の処理を特別扱い
- シフト演算（
a << i）の追加 - 配列のインデックスを修正（
tmp_m[7]を最終出力として使用）
修正後の検証結果
修正後のデザインで再度検証を実施した。結果は以下の通りである。
... 途中省略 ... SBY 16:06:27 [mult_bmc] engine_0: ## 0:02:54 Checking assertions in step 18.. SBY 16:06:38 [mult_bmc] engine_0: ## 0:03:05 Checking assumptions in step 19.. SBY 16:06:38 [mult_bmc] engine_0: ## 0:03:05 Checking assertions in step 19.. SBY 16:06:49 [mult_bmc] engine_0: ## 0:03:16 Checking assumptions in step 20.. SBY 16:06:49 [mult_bmc] engine_0: ## 0:03:16 Checking assertions in step 20.. SBY 16:06:59 [mult_bmc] engine_0: ## 0:03:26 Checking assumptions in step 21.. SBY 16:06:59 [mult_bmc] engine_0: ## 0:03:26 Checking assertions in step 21.. SBY 16:07:08 [mult_bmc] engine_0: ## 0:03:36 Checking assumptions in step 22.. SBY 16:07:08 [mult_bmc] engine_0: ## 0:03:36 Checking assertions in step 22.. SBY 16:07:19 [mult_bmc] engine_0: ## 0:03:46 Checking assumptions in step 23.. SBY 16:07:19 [mult_bmc] engine_0: ## 0:03:46 Checking assertions in step 23.. SBY 16:07:29 [mult_bmc] engine_0: ## 0:03:56 Checking assumptions in step 24.. SBY 16:07:29 [mult_bmc] engine_0: ## 0:03:56 Checking assertions in step 24.. SBY 16:07:39 [mult_bmc] engine_0: ## 0:04:06 Checking assumptions in step 25.. SBY 16:07:39 [mult_bmc] engine_0: ## 0:04:06 Checking assertions in step 25.. SBY 16:07:48 [mult_bmc] engine_0: ## 0:04:15 Checking assumptions in step 26.. SBY 16:07:48 [mult_bmc] engine_0: ## 0:04:15 Checking assertions in step 26.. SBY 16:07:56 [mult_bmc] engine_0: ## 0:04:23 Checking assumptions in step 27.. SBY 16:07:56 [mult_bmc] engine_0: ## 0:04:23 Checking assertions in step 27.. SBY 16:08:07 [mult_bmc] engine_0: ## 0:04:34 Checking assumptions in step 28.. SBY 16:08:07 [mult_bmc] engine_0: ## 0:04:34 Checking assertions in step 28.. SBY 16:08:17 [mult_bmc] engine_0: ## 0:04:44 Checking assumptions in step 29.. SBY 16:08:17 [mult_bmc] engine_0: ## 0:04:44 Checking assertions in step 29.. SBY 16:08:27 [mult_bmc] engine_0: ## 0:04:54 Checking assumptions in step 30.. SBY 16:08:27 [mult_bmc] engine_0: ## 0:04:54 Checking assertions in step 30.. SBY 16:08:36 [mult_bmc] engine_0: ## 0:05:03 Checking assumptions in step 31.. SBY 16:08:36 [mult_bmc] engine_0: ## 0:05:03 Checking assertions in step 31.. SBY 16:08:45 [mult_bmc] engine_0: ## 0:05:13 Checking assumptions in step 32.. SBY 16:08:46 [mult_bmc] engine_0: ## 0:05:13 Checking assertions in step 32.. SBY 16:08:54 [mult_bmc] engine_0: ## 0:05:22 Checking assumptions in step 33.. SBY 16:08:54 [mult_bmc] engine_0: ## 0:05:22 Checking assertions in step 33.. SBY 16:09:03 [mult_bmc] engine_0: ## 0:05:31 Checking assumptions in step 34.. SBY 16:09:03 [mult_bmc] engine_0: ## 0:05:31 Checking assertions in step 34.. SBY 16:09:13 [mult_bmc] engine_0: ## 0:05:40 Checking assumptions in step 35.. SBY 16:09:13 [mult_bmc] engine_0: ## 0:05:40 Checking assertions in step 35.. SBY 16:09:23 [mult_bmc] engine_0: ## 0:05:50 Checking assumptions in step 36.. SBY 16:09:23 [mult_bmc] engine_0: ## 0:05:50 Checking assertions in step 36.. SBY 16:09:35 [mult_bmc] engine_0: ## 0:06:02 Checking assumptions in step 37.. SBY 16:09:35 [mult_bmc] engine_0: ## 0:06:02 Checking assertions in step 37.. SBY 16:09:45 [mult_bmc] engine_0: ## 0:06:12 Checking assumptions in step 38.. SBY 16:09:45 [mult_bmc] engine_0: ## 0:06:12 Checking assertions in step 38.. SBY 16:09:56 [mult_bmc] engine_0: ## 0:06:23 Checking assumptions in step 39.. SBY 16:09:56 [mult_bmc] engine_0: ## 0:06:23 Checking assertions in step 39.. SBY 16:10:07 [mult_bmc] engine_0: ## 0:06:34 Status: passed SBY 16:10:07 [mult_bmc] engine_0: finished (returncode=0) SBY 16:10:07 [mult_bmc] engine_0: Status returned by engine: pass SBY 16:10:07 [mult_bmc] summary: Elapsed clock time [H:MM:SS (secs)]: 0:06:34 (394) SBY 16:10:07 [mult_bmc] summary: Elapsed process time [H:MM:SS (secs)]: 0:06:34 (394) SBY 16:10:07 [mult_bmc] summary: engine_0 (smtbmc z3) returned pass SBY 16:10:07 [mult_bmc] summary: engine_0 did not produce any traces SBY 16:10:07 [mult_bmc] DONE (PASS, rc=0)
うまくいったようだ。
