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 Vacuous Property (with a bug)

SystemVerilog Formal Verification

A state machine with a bug and a property whose trigger can never happen. Everything passes until the trigger is fixed.

Open in IDE
design.sv
// SVA form (used by commercial formal tools):
//   a_done: assert property (@(posedge clk) disable iff (rst) state == 2'd3 |=> state == IDLE);  // typo: DONE is 2
//   c_done: cover  property (@(posedge clk) disable iff (rst) state == 2'd3);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module fsm_vac (input clk, input rst, input start, input stop, output reg [1:0] state);
  localparam IDLE = 2'd0, RUN = 2'd1, DONE = 2'd2;
  always @(posedge clk)
    if (rst) state <= IDLE;
    else case (state)
      IDLE:    if (start) state <= RUN;
      RUN:     if (stop)  state <= DONE;
      DONE:               state <= RUN;     // bug
      default:            state <= IDLE;
    endcase

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // intended: after DONE the machine goes to IDLE
  // typo: compares with 3 instead of DONE (2), so the trigger never happens
  always @(posedge clk) if (!init && !$past(rst) && $past(state) == 2'd3) assert (state == IDLE);
  // cover for the trigger
  always @(posedge clk) if (!init && !$past(rst)) assert (!($past(state) == 2'd3));   // trigger reachable? 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.