Verilog 2001で実装されたBooth乗算器を調査する (6. SymbiYosysを用いた形式検証環境の構築と実行)

前章まででVerilatorによるシミュレーション検証を実施したが、つぎは形式検証（Formal Verification）をSymbiYosysを使用して実装してみよう。

Formal検証コードの実装

mul_1.vに以下のFormal検証コードを追加した：

`ifdef FORMAL
logic            r_result_valid;
always_ff @ (posedge clk, posedge reset) begin
  if (reset) begin
    r_result_valid <= 1'b0;
  end else begin
    r_result_valid <= req_valid;
  end
end

logic        [63: 0] x_u, y_u;
logic signed [63: 0] x_s, y_s;
logic signed [63: 0] model_result;
always_comb begin
  x_u = {32'b0, x};
  y_u = {32'b0, y};
  x_s = x_signed ? $signed({{32{x[31]}}, x}) : $signed(x_u);
  y_s = y_signed ? $signed({{32{y[31]}}, y}) : $signed(y_u);
  model_result = x_s * y_s;

  assert ((r_result_valid & (resp_result == model_result)) | !r_result_valid);
end
`endif // FORMAL

SymbiYosys設定ファイルの設計

以下の設定ファイル（booth_mult.sby）を作成した：

[options]
mode bmc
depth 40

[engines]
# smtbmc yices
# smtbmc boolector
# smtbmc bitwuzla
smtbmc z3
# smtbmc mathsat
# smtbmc cvc4
# smtbmc cvc5

[script]
read -sv -formal booth_mult.sv
prep -top booth_mult

[files]
booth_mult.sv

形式検証の実行結果

SymbiYosysを実行した結果、以下のログが出力された：

SBY 16:38:25 [booth_mult_bmc] base: Warning: Resizing cell port booth_mult.booth3.i from 32 bits to 1 bits.
SBY 16:38:25 [booth_mult_bmc] base: Warning: Resizing cell port booth_mult.booth2.i from 32 bits to 1 bits.
SBY 16:38:25 [booth_mult_bmc] base: Warning: Resizing cell port booth_mult.booth1.i from 32 bits to 1 bits.
SBY 16:38:25 [booth_mult_bmc] base: Warning: Resizing cell port booth_mult.booth0.i from 32 bits to 1 bits.
SBY 16:38:25 [booth_mult_bmc] base: finished (returncode=0)
SBY 16:38:25 [booth_mult_bmc] prep: starting process "cd booth_mult_bmc/model; yosys -ql design_prep.log design_prep.ys"
SBY 16:38:25 [booth_mult_bmc] prep: finished (returncode=0)
SBY 16:38:25 [booth_mult_bmc] smt2: starting process "cd booth_mult_bmc/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 16:38:25 [booth_mult_bmc] smt2: finished (returncode=0)
SBY 16:38:25 [booth_mult_bmc] engine_0: starting process "cd booth_mult_bmc; yosys-smtbmc -s z3 --presat --noprogress -t 40  --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 16:38:26 [booth_mult_bmc] engine_0: ##   0:00:00  Solver: z3
SBY 16:38:26 [booth_mult_bmc] engine_0: ##   0:00:00  Checking assumptions in step 0..

まだ実行中だ。