Synchronous FIFOs

The synchronous FIFO is the most verified block in hardware, and still a steady source of bugs: the full flag set one word early or late, a pointer that wraps wrongly, data overwritten when push and pop meet. A complete formal check of a FIFO has four parts: no overflow or underflow, flags consistent with the contents, data out in order, and a proof for every cycle. This article builds that check for a FIFO that tells full from empty by its pointers alone, and finds a capacity bug.

10 min read | Intermediate

What You'll Learn

• Write the complete property set for a FIFO
• Use a reference count kept by the formal code to check the flags
• Find the classic full-versus-empty pointer bug and fix it with an extra pointer bit
• Complete a FIFO proof with a helper invariant

The Property Set

• No overflow, no underflow: the number of stored words stays between 0 and the depth.
• Flags: full exactly when the FIFO holds the depth, empty exactly when it holds nothing.
• Data order: every word comes out once, unchanged and in order, checked with the tracked value from the data integrity article.
• Reachability: full and empty both happen, and push and pop in the same cycle happen in every fill level.

The count of stored words is the key to the first two. This FIFO has no count register, so the formal code keeps its own: a reference count n updated from the accepted pushes and pops. It is independent of the pointers, so it can judge them.

The Design: a Pointer-Only FIFO

module fifo_ptr (input clk, input rst, input push, input [7:0] din, input pop,
                 output [7:0] dout, output full, output empty);
  reg [7:0] mem [0:3];
  reg [1:0] wptr, rptr;
  assign empty = (wptr == rptr);
  assign full  = (wptr + 2'd1 == rptr);          // bug: this FIFO can only hold 3 words
  assign dout  = mem[rptr];
  wire do_push = push && !full;
  wire do_pop  = pop && !empty;
  always @(posedge clk)
    if (rst) begin
      wptr <= 2'd0; rptr <= 2'd0;
    end else begin
      if (do_push) begin mem[wptr] <= din; wptr <= wptr + 2'd1; end
      if (do_pop)  rptr <= rptr + 2'd1;
    end
endmodule

With 2-bit pointers into 4 entries, "pointers equal" means either empty or full: after 4 pushes the write pointer wraps around to the read pointer. The designer avoided the ambiguity by calling the FIFO full one word early. That works, but it silently turns a 4-entry FIFO into a 3-entry one, against the specification.

The Properties

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // reference count, kept by the formal code from the accepted operations
  reg [2:0] n = 3'd0;
  always @(posedge clk) n <= rst ? 3'd0 : n + do_push - do_pop;
  // specification: 4 entries, full exactly at 4, empty exactly at 0
  always @(*) if (!init) assert (n <= 3'd4);
  always @(*) if (!init) assert (full == (n == 3'd4));
  always @(*) if (!init) assert (empty == (n == 3'd0));
`endif

The run fails at step 4:

After three pushes, full is high while the reference count is 3. In a simulation this looks like normal back-pressure, and nothing breaks. Only a check of the flag against the specified depth notices the lost entry.

The Fix: One Extra Pointer Bit

The standard solution gives each pointer one more bit than the address needs. The low bits address the memory; the extra bit flips at every wrap. Equal pointers mean empty, and pointers that differ only in the extra bit mean full:

reg [2:0] wptr, rptr;                          // one extra bit tells full from empty
assign empty = (wptr == rptr);
assign full  = (wptr == {~rptr[2], rptr[1:0]});
assign dout  = mem[rptr[1:0]];
// ... mem[wptr[1:0]] <= din; wptr <= wptr + 3'd1; rptr <= rptr + 3'd1;

With it, the three assertions pass, and a meant-to-fail check assert (!full) fails at step 5, which shows the FIFO really fills up with 4 words.

The Proof

In prove mode, the fixed FIFO is UNKNOWN at first: the induction step starts from states where the reference count and the pointers disagree. The helper invariant states their relation:

// helper: the reference count equals the pointer difference
always @(*) if (!init) assert (n == wptr - rptr);

With it, k-induction proves all properties with k = 1. This helper, count equals write pointer minus read pointer, is the standard strengthening for every FIFO.

Running It in ChipVerify Lab

The example below is the pointer-only FIFO with the bug and the reference-count properties. It fails at step 4.

Common Mistakes