SymbiYosysを使ったBooth乗算器のフォーマル検証を試行する

より複雑なBooth乗算器に対して同様のフォーマル検証を試行してみる。

Booth乗算器は、符号付き数の乗算を効率的に実行するためのアルゴリズムであり、部分積の数を削減することで高速化を図る手法である。 このような複雑な設計に対してフォーマル検証がどこまで有効に機能するかを確認してみたい。

Booth乗算器の設計

module booth_mult
  (
   input         clk,
   input         reset,
   input         req_valid,
   input         req_in_1_signed,
   input         req_in_2_signed,
   input [31:0]  req_in_1,
   input [31:0]  req_in_2,
   output [63:0] resp_result
   );

フォーマル検証の設定

Booth乗算器の検証には、以下の設定ファイルを使用した：

[options]
mode bmc
depth 40

[engines]
smtbmc z3

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

[files]
booth_mult.v

アサーションの定義

一発で32ビットの乗算器を検証することはどう考えてもできないので、ステップ・バイ・ステップで検証をできないか試してみる。

1. 下位の8ビットは検証できているものとする
2. 次の8ビットは、下位が検証できているものとして検証する

logic        [15: 0] x_u, y_u;
logic signed [15: 0] x_s, y_s;
logic signed [15: 0] model_result;

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

  assume (resp_result[ 7: 0] == model_result[ 7: 0]);
  assert (resp_result[15: 8] == model_result[15: 8]);
end

検証の実行

検証を実行すると、以下のような状態になるのだが、まだ検証は完了していない。

SBY 16:23:49 [booth_mult_bmc] prep: finished (returncode=0)
SBY 16:23:49 [booth_mult_bmc] smt2: starting process "cd booth_mult_bmc/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 16:23:49 [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:23:49 [booth_mult_bmc] engine_0: ##   0:00:00  Solver: z3
SBY 16:23:49 [booth_mult_bmc] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY 16:24:49 [booth_mult_bmc] engine_0: ##   0:01:00  waiting for solver (1 minute)