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

SymbiYosysでラウンドロビンアービタを検証する

ラウンドロビンアービタは、複数のリクエストを公平に処理するための回路である。 SystemVerilogで実装したラウンドロビンアービタを、形式検証ツールであるSymbiYosysを使用して検証してみる。

ラウンドロビンアービタの実装

まず、N入力のラウンドロビンアービタを以下のように実装した。このコードは、テストを流して検証したわけではないが、まあ多分なんとなく動くと思う。

module rr_arbiter #(
  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);

logic [LG-1:0]         r_last_idx;
logic [LG-1:0]         w_idx_next;

always_comb begin
  w_idx_next = r_last_idx;

  for (int i = 1; i <= N; i++) begin: loop_arbiter
    if (i_req[(r_last_idx + i) % N]) begin
      w_idx_next = (r_last_idx + i) % N;
    end
  end
end

assign o_grant = (1 << w_idx_next);

always @(posedge i_clk or negedge i_rst_n) begin
  if (!i_rst_n) begin
    r_last_idx <= 'h0;
  end else begin
    r_last_idx <= w_idx_next;
  end
end

`ifdef FORMAL
always_comb begin
  assert ((o_grant & (o_grant - 1)) == 0);
  assert (!(~|i_req) || (o_grant == 0));
end
`endif // FORMAL

endmodule // rr_arbiter

アサーションの説明

この実装では、以下の2つのアサーションを設定している：

(o_grant & (o_grant - 1)) == 0: o_grantは常に1ビットのみが出力されることを保証する。
(!(~|i_req) || (o_grant == 0)): i_reqがゼロの時は、何も出力されないことを保証する。

SymbiYosysの設定

SymbiYosysのコンフィグレーションを以下のように設定した。

BMCの場合

[options]
mode bmc
depth 40

[engines]
smtbmc z3

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

[files]
rr_arbiter.sv

UMCの場合

[options]
mode prove

[engines]
smtbmc z3

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

[files]
rr_arbiter.sv

検証の実行

実際に検証を実行してみる。

$ sby -f rr_arbiter_bmc.sby

しかし、残念ながら検証が完了しない。状態遷移が発生するデザインは、形式検証が難しい場合がある。

SBY 15:34:27 [rr_arbiter_bmc] prep: finished (returncode=0)
SBY 15:34:27 [rr_arbiter_bmc] smt2: starting process "cd rr_arbiter_bmc/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:34:27 [rr_arbiter_bmc] smt2: finished (returncode=0)
SBY 15:34:27 [rr_arbiter_bmc] engine_0: starting process "cd rr_arbiter_bmc; yosys-smtbmc -s z3 --presat --noprogress -t 40  --append 0 --dump-vcd engine_0/trace.vcd --dump-yw engine_0/trace.yw --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 15:34:27 [rr_arbiter_bmc] engine_0: ##   0:00:00  Solver: z3
SBY 15:34:27 [rr_arbiter_bmc] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY 15:35:27 [rr_arbiter_bmc] engine_0: ##   0:01:00  waiting for solver (1 minute)
SBY 15:39:27 [rr_arbiter_bmc] engine_0: ##   0:05:00  waiting for solver (5 minutes)
SBY 15:44:27 [rr_arbiter_bmc] engine_0: ##   0:10:00  waiting for solver (10 minutes)
SBY 15:49:27 [rr_arbiter_bmc] engine_0: ##   0:15:00  waiting for solver (15 minutes)