FVO — Formal Verification Online
Lesson 6.2 · FPV for Bug Hunting and Signoff

The example: a synchronous FIFO

Few blocks are as common — or as often subtly broken — as FIFOs. Ours is a single-clock, first-word-fall-through FIFO: rdata always shows the oldest entry while the FIFO is not empty.

Specification

  1. A push writes wdata unless the FIFO is full; a push while full is dropped (even if pop is also high).
  2. A pop removes the oldest entry unless the FIFO is empty; a pop while empty is ignored.
  3. Data leaves in the same order it entered, unmodified.
  4. count is the number of stored entries; full ⇔ count = DEPTH; empty ⇔ count = 0.
  5. DEPTH must be a power of two.
sync_fifo.sv
// sync_fifo.sv — single-clock FWFT FIFO (DEPTH must be a power of two)
module sync_fifo #(
  parameter int WIDTH = 8,
  parameter int DEPTH = 4
) (
  input  logic             clk,
  input  logic             rst,
  input  logic             push,
  input  logic [WIDTH-1:0] wdata,
  input  logic             pop,
  output logic [WIDTH-1:0] rdata,
  output logic             full,
  output logic             empty,
  output logic [$clog2(DEPTH+1)-1:0] count
);
  localparam int AW = $clog2(DEPTH);
  localparam int CW = $clog2(DEPTH + 1);

  logic [WIDTH-1:0] mem [DEPTH];
  logic [AW-1:0]    wptr, rptr;
  logic             do_push, do_pop;

  assign do_push = push && !full;      // spec 1: push while full is dropped
  assign do_pop  = pop  && !empty;     // spec 2: pop while empty is ignored

  always_ff @(posedge clk) begin
    if (rst) begin
      wptr  <= '0;
      rptr  <= '0;
      count <= '0;
    end else begin
      if (do_push) begin
        mem[wptr] <= wdata;
        wptr      <= wptr + 1'b1;     // wraps naturally: DEPTH is a power of two
      end
      if (do_pop) rptr <= rptr + 1'b1;
      count <= count + CW'(do_push) - CW'(do_pop);
    end
  end

  assign rdata = mem[rptr];
  assign empty = (count == '0);
  assign full  = (count == CW'(DEPTH));
endmodule
Was this page helpful?

Tip: select any text on the page before clicking Report and it will be quoted in your report.