カテゴリインデックス：https://msyksphinz.hatenablog.com/entry/2024/12/14/040000

SymbiYosysを使った乗算器の形式検証

SymbiYosysを使用して乗算器の形式検証を行ってみる。

検証対象の乗算器

検証対象の乗算器は以下のようなVerilogコードで記述されている。8ビットの入力a, bを受け取り、16ビットの出力mを生成する単純な乗算器である。

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
  tmp_m[0] = 'h0;
  for (int i = 0; i < 8; i++) begin
    if (b[i]) begin
      tmp_m[i+1] = tmp_m[i] + a;
    end else begin
      tmp_m[i+1] = tmp_m[i];
    end
  end
end
assign m = tmp_m[8];

`ifdef FORMAL
always_comb begin
  assert (m == a * b);
end
`endif // FORMAL

endmodule // mult

この乗算器は、シフト加算アルゴリズムを使用して実装されている。入力bの各ビットを順番にチェックし、ビットが1の場合に入力aを加算する方式である。

見ればわかるが、この乗算器は普通に実装が間違っており、正しい結果が得られない(普通にミスした)。

形式検証の設定

形式検証は以下の設定で実行した：

[options]
mode bmc
depth 40

[engines]
smtbmc z3

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

[files]
mult.v

BMC（Bounded Model Checking）モードを使用
検証深度は40
SMTソルバーとしてZ3を使用

検証結果

検証を実行したところ、以下のような結果が得られた：

SBY 15:47:03 [mult_bmc] engine_0: ##   0:00:00  BMC failed!
SBY 15:47:03 [mult_bmc] engine_0: ##   0:00:00  Assert failed in mult: mult.v:24.3-24.22 (_witness_.check_assert_mult_v_24_14)

検証は失敗し、アサーション違反が検出された。当たり前だ。波形を取得して、表示してみた。このように、不具合が起きている波形を取得して確認することができる。