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

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

前回実装したアービタを検証するために、フォーマルの記述を追加していく：

logic [N-1: 0] r_sim_priority_oh;
logic [N-1: 0] w_sim_priority_oh_next;
logic [N-1: 0] w_sim_temp_priority_oh[N];
logic [N-1: 0] w_sim_grant_oh;
logic found;

always @(posedge i_clk or negedge i_rst_n) begin
  if (!i_rst_n) begin
    r_sim_priority_oh <= {{{(N-1){1'b0}}, 1'b1}};
  end else begin
    r_sim_priority_oh <= w_sim_priority_oh_next;
  end
end

assign w_sim_temp_priority_oh[0] = r_sim_priority_oh;
generate for (genvar i = 1; i < N; i = i+1) begin: loop_sim_priority_oh
  assign w_sim_temp_priority_oh[i] = {r_sim_priority_oh[N-1-i: 0], r_sim_priority_oh[N-1: N-i]};
end endgenerate


always_comb begin
  w_sim_priority_oh_next = r_sim_priority_oh;
  w_sim_grant_oh = 0;
  found = 0;
  for (int i = 0; i < N; i = i+1) begin: loop_sim_grant_oh
    if (found == 0 && |(w_sim_temp_priority_oh[i] & i_req)) begin
      w_sim_grant_oh = w_sim_temp_priority_oh[i];
      w_sim_priority_oh_next = w_sim_temp_priority_oh[(i+1)%N];
      found = 1;
    end
  end

  // if (found && (w_sim_grant_oh != o_grant)) begin
  //   $fatal(1, "w_sim_grant_oh != o_grant: %b != %b", w_sim_grant_oh, o_grant);
  // end
`ifdef FORMAL
  assert (w_sim_grant_oh == o_grant);
`endif // FORMAL
end

最後のフォーマル記述で、 assert (w_sim_grant_oh == o_grant); により、正しくGrantが生成されるのを確認したい。

実行してみると、以下のようになった。ちょっとまだアサーションに問題があるかな。

SBY 16:49:55 [rr_arbiter2_bmc] engine_0: finished (returncode=1)
SBY 16:49:55 [rr_arbiter2_bmc] engine_0: Status returned by engine: FAIL
SBY 16:49:55 [rr_arbiter2_bmc] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 16:49:55 [rr_arbiter2_bmc] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 16:49:55 [rr_arbiter2_bmc] summary: engine_0 (smtbmc) returned FAIL
SBY 16:49:55 [rr_arbiter2_bmc] summary: counterexample trace: rr_arbiter2_bmc/engine_0/trace.vcd
SBY 16:49:55 [rr_arbiter2_bmc] summary:   failed assertion rr_arbiter2._witness_.check_assert_rr_arbiter2_sv_85_38 at rr_arbiter2.sv:85.3-85.37
SBY 16:49:55 [rr_arbiter2_bmc] DONE (FAIL, rc=2)