Ready-to-run snippets

Code Examples

Ready-to-run Verilog, SystemVerilog, and UVM examples. Click any to open it live in the IDE.

← All examples

FV Capstone: round-robin arbiter

SystemVerilog Formal Verification

The fixed round-robin arbiter with safety, fairness and a hold assumption; covers as commented meant-to-fail checks.

Open in IDE
design.sv
// SVA form of the fairness rule (used by commercial formal tools):
//   a_fair3: assert property (@(posedge clk) disable iff (rst) req[3] |-> ##[0:4] gnt[3]);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module rr_arb (input clk, input rst, input [3:0] req, output reg [3:0] gnt);
  // round-robin arbiter: after a grant, the next requester in order has the highest priority
  reg [1:0] last;                       // index of the last granted requester
  reg [3:0] nxt;
  integer i;
  always @(*) begin
    nxt = 4'b0000;
    for (i = 3; i >= 1; i = i - 1)      // search last+1, last+2, last+3, then last itself
      if (req[(last + i) % 4]) nxt = 4'b0001 << ((last + i) % 4);
    if (nxt == 4'b0000 && req[last]) nxt = 4'b0001 << last;
  end
  always @(posedge clk)
    if (rst) begin
      gnt <= 4'b0000; last <= 2'd3;
    end else begin
      gnt <= nxt;
      if (nxt[0]) last <= 2'd0;
      if (nxt[1]) last <= 2'd1;
      if (nxt[2]) last <= 2'd2;
      if (nxt[3]) last <= 2'd3;
    end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // requests are held until granted
  genvar k;
  generate for (k = 0; k < 4; k = k + 1) begin : hold
    always @(posedge clk) if (!init && !$past(rst) && $past(req[k]) && !gnt[k]) assume (req[k]);
  end endgenerate
  // at most one grant, and only to a requester that asked
  always @(*) if (!init) assert ($onehot0(gnt));
  always @(posedge clk) if (!init && !$past(rst)) assert ((gnt & ~$past(req)) == 4'b0000);
  // fairness: every requester is served within 4 cycles of asking
  reg [2:0] w0 = 0, w1 = 0, w2 = 0, w3 = 0;
  always @(posedge clk) begin
    w0 <= (rst || gnt[0] || !req[0]) ? 3'd0 : w0 + 3'd1;
    w1 <= (rst || gnt[1] || !req[1]) ? 3'd0 : w1 + 3'd1;
    w2 <= (rst || gnt[2] || !req[2]) ? 3'd0 : w2 + 3'd1;
    w3 <= (rst || gnt[3] || !req[3]) ? 3'd0 : w3 + 3'd1;
  end
  always @(*) if (!init) assert (w0 <= 3'd4 && w1 <= 3'd4 && w2 <= 3'd4 && w3 <= 3'd4);
  // covers as meant-to-fail checks: uncomment one at a time; a failure is a trace that reaches the situation
  // always @(*) if (!init) assert (!gnt[3]);                  // requester 3 is granted
  // always @(*) if (!init) assert (!(req == 4'b1111));        // all four request together
  // always @(*) if (!init) assert (!(w3 == 3'd4));            // requester 3 waits the worst case
`endif
endmodule
Admin mode — edit and delete controls are visible on each row. Use the IDE to add new snippets via File → Save as Snippet.