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

形式検証ツールSymbiYosysを用いたFIFOの検証

検証対象のFIFO

検証対象としたFIFOは、以下の特徴を持つシンプルな実装である：

データ幅：8ビット（パラメータ化可能）
エントリ数：4
制御信号：プッシュ（書き込み）、ポップ（読み出し）
状態信号：フル、エンプティ

実装コード

module fifo4
  #(
    parameter WIDTH = 8
    )
(
 input logic              i_clk,
 input logic              i_rst_n,
 input logic              i_push,
 input logic              i_pop,
 input logic [WIDTH-1:0]  i_din,
 output logic [WIDTH-1:0] o_dout,

 output logic             o_full,
 output logic             o_empty
);
logic [WIDTH-1:0]             r_mem [3:0];
logic [ 2: 0]                 rd_ptr, wr_ptr, r_count;

assign o_full  = (r_count == 'h4);
assign o_empty = (r_count == 'h0);

always_ff @(posedge i_clk or negedge i_rst_n) begin
  if (!i_rst_n) begin
    rd_ptr  <= 'h0;
    wr_ptr  <= 'h0;
    r_count <= 'h0;
  end else begin
    if (i_push && !o_full) begin
      r_mem[wr_ptr] <= i_din;
      wr_ptr        <= wr_ptr + 1;
    end
    if (i_pop & !o_empty) begin
      o_dout <= r_mem[rd_ptr];
      rd_ptr <= rd_ptr + 1;
    end
    case ({i_push && !o_full, i_pop && !o_empty})
      2'b10: r_count <= r_count + 'h1;
      2'b01: r_count <= r_count - 'h1;
      default: ;
    endcase // case ({i_push && !o_full, i_pop && !o_empty})
  end // else: !if(!i_rst_n)
end // always @ (posedge i_clk or negedge i_rst_n)

`ifdef FORMAL
wire push = i_push & !o_full;
wire pop  = i_pop  & !o_empty;
always_comb begin
  // Doesn't happen full & push
  assert ((o_full & push) == 0);
  // Doesn't happen empty & pop
  assert ((o_empty & pop) == 0);
end
`endif // FORMAL

endmodule // fifo4

形式検証の設定

形式検証には、以下の設定ファイルを使用した：

[options]
mode bmc
depth 40

[engines]
smtbmc z3

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

[files]
fifo4.sv

主な設定項目： - 検証モード：BMC（Bounded Model Checking） - 検証深度：40ステップ - 使用エンジン：Z3

検証結果

形式検証の結果、以下のことが確認できた：

フル状態でのプッシュ操作が発生しないこと
エンプティ状態でのポップ操作が発生しないこと

検証ログ：

SBY 16:36:59 [fifo4_bmc] engine_0: Status: passed
SBY 16:36:59 [fifo4_bmc] engine_0: finished (returncode=0)
SBY 16:36:59 [fifo4_bmc] engine_0: Status returned by engine: pass