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 Covers for a State Machine

SystemVerilog Formal Verification

One cover per state and one for an err/stop collision. The collision is unreachable because of a priority bug.

Open in IDE
design.sv
// SVA form of the covers (used by commercial formal tools):
//   c_coll: cover property (@(posedge clk) disable iff (rst) state == RUN && err && stop ##1 state == FAIL);
// The lab panel runs assertions only: the meant-to-fail assertion below asks the same question.
module fsm_cover (input clk, input rst, input start, input stop, input err,
                  output reg [1:0] state);
  localparam IDLE = 2'd0, RUN = 2'd1, DONE = 2'd2, FAIL = 2'd3;
  always @(posedge clk)
    if (rst) state <= IDLE;
    else case (state)
      IDLE: if (start)      state <= RUN;
      RUN:  if (stop)       state <= DONE;
            else if (err)   state <= FAIL;   // bug: stop has priority, but the spec says err wins
      DONE:                 state <= IDLE;
      FAIL: if (!err)       state <= IDLE;
    endcase

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // environment: the error line is only active while running
  always @(*) if (!init && state != RUN && state != FAIL) assume (!err);
  // one cover per state, and one for the err/stop collision (SymbiYosys cover mode, commercial tools)
  always @(posedge clk) if (!init) cover (state == RUN);
  always @(posedge clk) if (!init) cover (state == DONE);
  always @(posedge clk) if (!init) cover (state == FAIL);
  always @(posedge clk) if (!init && !$past(rst)) cover ($past(state) == RUN && $past(err) && $past(stop) && state == FAIL);
  // the same question for the lab panel: meant to fail if the collision case is reachable
  always @(posedge clk) if (!init && !$past(rst)) assert (!($past(state) == RUN && $past(err) && $past(stop) && state == FAIL));   // meant to fail
`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.