オープンソース形式検証ツールSymbiYosysを用いて形式検証に入門する (2. Failするパタンの検証)

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

まずは基本的なフォーマルを勉強するために、SymbiYosysを使ってALUを検証してみたい。 以下にHalf Adder & Half Adder & ALUを構成するデザインを作った。

• ha.v

module ha
// 途中省略
endmodule // ha

• fa.v

module fa
// 途中省略
endmodule // fa

• alu.v

module alu
  (
   input logic [ 7: 0] a,
   input logic [ 7: 0] b,
   output logic [ 8: 0] s
   );

logic [ 7: 0]           c;
fa fa0 (.a(a[0]), .b(b[0]), .cin(1'b0), .s(s[0]), .cout(c[0]));
generate for (genvar idx = 1; idx < 8; idx++) begin : GEN_loop
  fa fa0 (.a(a[idx]), .b(b[idx]), .cin(c[idx-1]), .s(s[idx]), .cout(c[idx]));
end endgenerate

assign s[8] = c[7];

これに対して、Formal用のアサーションを実行する：

`ifdef FORMAL
always_comb begin
  assert (s == {1'b0, a} + {1'b0, b});
end
`endif // FORMAL

これに対してSymbiYosysを適用する。以下がスクリプト：

[options]
mode bmc
depth 40

[engines]
smtbmc z3

[script]
read -sv -formal ha.v
read -sv -formal fa.v
read -sv -formal alu.v
prep -top alu

[files]
ha.v
fa.v
alu.v

これを実行すると、SymbiYosysはフォーマル検証を成功させたようだ。

$ sby -f alu_bmc.sby                                                              

SBY  1:03:08 [alu_bmc] engine_0: ##   0:00:00  Checking assumptions in step 39..
SBY  1:03:08 [alu_bmc] engine_0: ##   0:00:00  Checking assertions in step 39..
SBY  1:03:08 [alu_bmc] engine_0: ##   0:00:00  Status: passed
SBY  1:03:08 [alu_bmc] engine_0: finished (returncode=0)
SBY  1:03:08 [alu_bmc] engine_0: Status returned by engine: pass
SBY  1:03:08 [alu_bmc] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  1:03:08 [alu_bmc] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  1:03:08 [alu_bmc] summary: engine_0 (smtbmc z3) returned pass
SBY  1:03:08 [alu_bmc] summary: engine_0 did not produce any traces
SBY  1:03:08 [alu_bmc] DONE (PASS, rc=0)