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 Arbiter Starvation (with a bug)

SystemVerilog Formal Verification

A fixed-priority arbiter that starves requester 1. Bounded liveness req[1] |-> ##[0:4] gnt[1] finds it.

Open in IDE
design.sv
// SVA form of the properties (used by commercial formal tools):
//   m_hold:  assume property (@(posedge clk) disable iff (rst) req[1] && !gnt[1] |=> req[1]);
//   a_bound: assert property (@(posedge clk) disable iff (rst) req[1] |-> ##[0:4] gnt[1]);
//   a_safe:  assert property (@(posedge clk) disable iff (rst) gnt != 2'b11);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module arb2 (input clk, input rst, input [1:0] req, output reg [1:0] gnt);
  // two requesters; a grant lasts one cycle
  always @(posedge clk)
    if (rst)         gnt <= 2'b00;
    else if (req[0]) gnt <= 2'b01;      // bug: fixed priority, requester 1 can starve
    else if (req[1]) gnt <= 2'b10;
    else             gnt <= 2'b00;

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // a request is held until it is granted
  always @(posedge clk) if (!init && !$past(rst) && $past(req[0]) && !gnt[0]) assume (req[0]);
  always @(posedge clk) if (!init && !$past(rst) && $past(req[1]) && !gnt[1]) assume (req[1]);
  // bounded liveness: req[1] |-> ##[1:4] gnt[1]
  reg [2:0] wait1 = 3'd0;
  always @(posedge clk) wait1 <= (rst || gnt[1] || !req[1]) ? 3'd0 : wait1 + 3'd1;
  always @(posedge clk) if (!init) assert (wait1 <= 3'd4);
  // safety: never two grants
  always @(posedge clk) if (!init) assert (gnt != 2'b11);
`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.