オープンソース形式検証ツールSymbiYosysを用いて形式検証に入門する (4. レジスタの付いたALUの検証)

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

基本的なALUの形式検証ができたので、今度はレジスタ付きのデザインを考えてみよう。 以下のデザインは、入力信号が入ってから2サイクル後に演算結果が出てくる：

always_ff @ (posedge i_clk, negedge i_reset_n) begin
  if (!i_reset_n) begin
    r1_a <= 'h0;
    r1_b <= 'h0;
  end else begin
    r1_a <= a;
    r1_b <= b;
  end
end

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

always_ff @ (posedge i_clk, negedge i_reset_n) begin
  if (!i_reset_n) begin
    s <= 'h0;
  end else begin
    s <= {w1_c[7], w1_s};
  end
end

これを検証するためには、以下の形式検証の記述を実装することになるだろう。

• 最初にi_reset_nはリセット状態であるとする。

initial begin
  assume(!i_reset_n);
end

• 2サイクル後にaとbの値が`sと結果が一致するはずである(ただし、2サイクル前からリセットが解除されていること)

always @(posedge i_clk) begin
  if ($past(i_reset_n, 2) && $past(i_reset_n) && i_reset_n) begin
    assert(s == $past({1'b0, a} + {1'b0, b}, 2));
  end
end

この結果、SymbiYosysの形式検証がPASSできた。

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