簡単なVerilogの回路実装をSymbiYosysのフォーマル検証を試す (1. ラウンドロビンアービタの設計)

SymbiYosysの能力を検証するために、簡単なサンプルデザインを作ってフォーマル検証を行っていく。

まずは、以下のような形のラウンドロビンアービタを作ったうえで、機能検証を行う。

module rr_arbiter2 #(
    parameter N = 4
)
(
    input logic i_clk,
    input logic i_rst_n,
    input logic [N-1:0] i_req,
    output logic [N-1:0] o_grant
);

localparam LG = $clog2(N);

// Current aoccepted index
logic [N-1: 0] r_pri_accepted_lo; // Priority bit: Leading One 11111000

// Generate LZ bit
logic [N*2-1: 0] w_mask_[LG:0];
logic [N*2-1: 0] w_mask; // accepted_or = 11111111_11111000
assign w_mask_[0] = {{N{1'b1}}, r_pri_accepted_lo} & {i_req, i_req};
generate for (genvar i = 1; i <= LG; i = i+1) begin: loop_mask
  assign w_mask_[i] = w_mask_[i-1] | w_mask_[i-1] << (1 << (i-1));
end endgenerate
assign w_mask = w_mask_[LG] | w_mask_[LG] << (1 << (LG));

logic [N*2-1: 0] w_req_masked_oh;
assign w_req_masked_oh = w_mask ^ (w_mask << 1);

logic [N-1: 0]  w_req;
assign w_req = (|w_req_masked_oh[N-1:0]) ? w_req_masked_oh[N-1:0] : w_req_masked_oh[N*2-1:N];

assign o_grant = w_req;

logic [N*2-1: 0] w_pri_accepted_lo_next_;
logic [  N-1: 0] w_pri_accepted_lo_next;
assign w_pri_accepted_lo_next_ = w_mask << 1;
assign w_pri_accepted_lo_next  = w_pri_accepted_lo_next_[N-1:0] == 'h0 ?w_pri_accepted_lo_next_[N*2-1:N] :
                                 w_pri_accepted_lo_next_[N-1:0] & w_pri_accepted_lo_next_[N*2-1:N];

always @(posedge i_clk or negedge i_rst_n) begin
  if (!i_rst_n) begin
    r_pri_accepted_lo <= {N{1'b1}};
  end else begin
    if (|i_req) begin
      r_pri_accepted_lo <= w_pri_accepted_lo_next;
    end
  end
end

endmodule

適当にテストパタンを流した結果。多分なんとなく動作している。

./obj_dir/Vtb_rr_arbiter2
                  15 w_req = 0000, w_grant = 0000
                  25 w_req = 0100, w_grant = 0100
                  35 w_req = 1100, w_grant = 1000
                  45 w_req = 0010, w_grant = 0010
                  55 w_req = 0100, w_grant = 0100
                  65 w_req = 1000, w_grant = 1000
                  75 w_req = 1100, w_grant = 0100
                  85 w_req = 0110, w_grant = 0010
                  95 w_req = 0100, w_grant = 0100
                 105 w_req = 0111, w_grant = 0001
                 115 w_req = 0011, w_grant = 0010
                 125 w_req = 0001, w_grant = 0001
                 135 w_req = 0001, w_grant = 0001
                 145 w_req = 0101, w_grant = 0100
                 155 w_req = 0010, w_grant = 0010
                 165 w_req = 0010, w_grant = 0010
                 175 w_req = 0101, w_grant = 0100
                 185 w_req = 0010, w_grant = 0010
                 195 w_req = 0110, w_grant = 0100
                 205 w_req = 1101, w_grant = 1000
- tb_rr_arbiter2.sv:25: Verilog $finish