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 Request Controller FSM (with a bug)

SystemVerilog Formal Verification

A controller with a 4-cycle timeout whose timer is not cleared on a new request.

Open in IDE
design.sv
// SVA form of the properties (used by commercial formal tools):
//   a_legal: assert property (@(posedge clk) disable iff (rst) state != 2'd3);
//   a_early: assert property (@(posedge clk) disable iff (rst) $rose(err) |-> $past(state == WAIT, 4));
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module req_fsm (input clk, input rst, input req, input ack, input clr,
                output busy, output err, output reg [1:0] state);
  // IDLE -> WAIT on req; WAIT -> IDLE on ack; WAIT -> ERR after 4 cycles without ack; ERR -> IDLE on clr
  localparam IDLE = 2'd0, WAIT = 2'd1, ERR = 2'd2;
  reg [2:0] t;
  assign busy = (state == WAIT);
  assign err  = (state == ERR);
  always @(posedge clk)
    if (rst) begin
      state <= IDLE; t <= 3'd0;
    end else case (state)
      IDLE: if (req) state <= WAIT;                     // bug: t is not cleared here
      WAIT: if (ack)            begin state <= IDLE; end
            else if (t == 3'd3) begin state <= ERR;  t <= 3'd0; end
            else                      t <= t + 3'd1;
      ERR:  if (clr) state <= IDLE;
      default: state <= IDLE;
    endcase

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // legal states only
  always @(*) if (!init) assert (state != 2'd3);
  // helper: how long the machine has been waiting
  reg [3:0] w = 4'd0;
  always @(posedge clk) w <= (rst || state != WAIT) ? 4'd0 : w + 4'd1;
  // ERR only after 4 cycles of waiting without ack
  always @(posedge clk) if (!init && !$past(rst) && err && !$past(err)) assert ($past(w) == 4'd3);
  // never stuck in WAIT: at most 4 cycles
  always @(*) if (!init) assert (w <= 4'd4);
`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.