Capstone: Verify a FIFO

This capstone verifies a FIFO completely: flags against a reference count, data order with a tracked value, covers, and a full proof by induction, with the helper invariants that the proof needs. It brings together the techniques of Chapters 3 to 8 on one design. The FIFO is parameterized; the proof uses 4 entries of 8 bits and holds for the logic of any size written the same way.

12 min read | Intermediate

What You'll Learn

• Assemble a complete property set for a FIFO from its specification
• Run a bounded check with covers as the first milestone
• Strengthen the properties round by round until the induction step passes
• Run both halves of the proof in ChipVerify Lab

The Design

The FIFO from the synchronous FIFOs article, with an extra wrap bit on each pointer and two parameters, data width W and address width AW:

module fifo_p #(parameter W = 8, parameter AW = 2) (input clk, input rst, input push, input [W-1:0] din, input pop,
                                                     output [W-1:0] dout, output full, output empty);
  reg [W-1:0] mem [0:(1<

Milestone 1: The Property Set

• Reference count n, updated from accepted pushes and pops.
• Flags: full exactly when n is the depth, empty exactly when it is 0.
• Order: a tracked word magic comes out when it reaches the head.
• Covers: full, empty after full, push and pop in the same cycle while full, magic leaving the FIFO.

No assumptions are needed: push, pop and din are free, because the FIFO itself must reject a push when full and a pop when empty. At depth 10, all properties pass and the covers are reached, full by step 5 and magic leaving by step 2. That is a solid bounded result. It is not yet a proof.

Milestone 2: The Proof

Prove mode returns UNKNOWN. Strengthening proceeds in rounds, as in the strengthening invariants article:

1. Count and pointers. The induction trace starts with a reference count that does not match the pointers. Helper: n == wptr - rptr, computed in AW + 1 bits so that the subtraction wraps like the pointers. Still UNKNOWN.
2. Where the tracked word is. The next trace starts with magic marked as tracked although it is not in the FIFO at all: the FIFO is empty. Helper: while tracking, ahead is less than n, and the memory at rptr + ahead holds magic. Still UNKNOWN.
3. Range. The next trace starts with n = 5, one more than the depth, with pointers that agree with it modulo 8. Helper: n is at most the depth. Now the proof passes with k = 1.

SBY [run] summary: engine_0 (smtbmc bitwuzla) returned pass for basecase
SBY [run] summary: engine_0 (smtbmc bitwuzla) returned pass for induction
SBY [run] summary: successful proof by k-induction.

The PDR engine proves the original properties without any helper. The helpers are still worth keeping: they document exactly how the FIFO works, and they make the proof fast and robust when the design changes.

Running It in ChipVerify Lab

The example collects the properties and helpers into single signals, so that both halves of the proof use exactly the same set:

  // the properties
  wire p_flags = (full == (n == (1 << AW))) && (empty == (n == 0));
  wire p_order = !(tracking && ahead == 0 && do_pop) || dout == magic;
  // the helpers that make them inductive
  wire [AW:0]   diff = wptr - rptr;
  wire [AW-1:0] mpos = rptr[AW-1:0] + ahead[AW-1:0];
  wire h_count = (n == diff) && (n <= (1 << AW));
  wire h_magic = !tracking || (ahead < n && mem[mpos] == magic);
  wire all_ok  = p_flags && p_order && h_count && h_magic;
`ifndef INDUCTION_STEP
  // base case: from reset
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init && !rst) assert (all_ok);
`else
  // induction step, K = 1: start anywhere, all properties hold in step 0, check step 1
  always @(*) assume (!rst);
  reg [7:0] step = 8'd0;
  always @(posedge clk) step <= step + 8'd1;
  always @(*) if (step < 8'd1) assume (all_ok);
  always @(*) if (step == 8'd1) assert (all_ok);
`endif

Run the base case at depth 10, then uncomment the `define INDUCTION_STEP line and run the step at depth 2. Both pass: the FIFO is proven. Remove any one helper from all_ok and the step fails at step 1.

One trap is worth knowing. The reference count and the tracking registers in the example have no initial values. If they had, such as reg [AW+1:0] n = 0;, the formal tool would start the induction step with n = 0 and tracking = 0, which is not "anywhere" at all, and the step would pass even without helpers. Formal-only registers that take part in the step must start free.

Common Mistakes