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 FIFO Counter (with a bug)

SystemVerilog Formal Verification

The occupancy counter of a 4-entry FIFO goes up to 5. Read the counterexample, find the bug and fix it.

Open in IDE
design.sv
module fifo_count (input clk, input rst, input push, input pop,
                   output reg [2:0] count, output full, output empty);
  assign full  = (count == 3'd5);     // bug: a 4-entry FIFO is full at 4
  assign empty = (count == 3'd0);
  always @(posedge clk)
    if (rst)                count <= 3'd0;
    else if (push && !full) count <= count + 3'd1;
    else if (pop && !empty) count <= count - 3'd1;

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(posedge clk) if (!init) assert (count <= 3'd4);
`endif
endmodule

// SVA form of the property (used by commercial formal tools):
//   a_count: assert property (@(posedge clk) disable iff (rst) count <= 3'd4);
// The open-source engine in ChipVerify Lab reads the equivalent block above.
Admin mode — edit and delete controls are visible on each row. Use the IDE to add new snippets via File → Save as Snippet.