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 Coverage Closure: classify the holes

SystemVerilog Formal Verification

Four simulation coverage holes of the request controller as meant-to-fail checks. Activate them one at a time.

Open in IDE
design.sv
// SVA form: each hole is a cover, e.g.  c_ack: cover property (@(posedge clk) disable iff (rst) busy && ack);
// 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) begin state <= WAIT; t <= 3'd0; end
      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);
  // coverage holes from simulation, as meant-to-fail checks: a failure gives a trace (reachable),
  // a pass means unreachable within the depth (prove it before excluding the point)
  always @(*) if (!init) assert (!(busy && ack));                       // hole 1: ack while waiting
  // always @(*) if (!init) assert (!(err && req));                    // hole 2: request while in ERR
  // always @(*) if (!init) assert (!(busy && err));                   // hole 3: busy and error together
  // always @(*) if (!init) assert (!(state == 2'd2 && t != 3'd0));    // hole 4: ERR with the timer running
`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.