Synchronous FIFO — Simulated, Proven, Synthesized

A parameterized FWFT FIFO treated the way you'd treat real IP: three independent checks, all gated in CI.

---

Why I built this

FIFOs look simple on paper. In silicon they're where overflow, off-by-one counts, and fall-through hazards actually show up.

I wanted one clean module I could reuse elsewhere (it ended up in the buffered UART) with evidence that goes beyond "the testbench passed today."

                ┌────────────────────────────────────────────┐
   wr_en ──────►│                                            │──────► rd_data (FWFT)
   wr_data ────►│      sync_fifo  (WIDTH × DEPTH)            │◄────── rd_en
   full  ◄──────│      single clock · registered count       │──────► empty
                │                                            │──────► count
                └────────────────────────────────────────────┘

WIDTH and DEPTH (power of two) are parameters. First-word fall-through read. Simultaneous read+write at any occupancy.

Verification stack

flowchart TB
    RTL[rtl/sync_fifo.v]
    RTL --> SIM[Simulation<br/>994 scoreboard checks]
    RTL --> FORM[Formal — SymbiYosys + z3<br/>overflow · flags · data integrity]
    RTL --> SYN[Synthesis — Yosys<br/>352 cells]
    SIM & FORM & SYN --> CI[GitHub Actions<br/>every push]

Loading

1. Simulation (make test)

A software queue mirrors every accepted write; every read is checked against it.

Directed phases: fill-to-full, blocked write, drain-to-empty, blocked read, simultaneous R/W streaming — then 2000 cycles of randomized traffic with random stalls.

994 comparisons, 0 mismatches.

2. Formal (make formal)

Simulation covers the cases you think of. Formal asks whether the properties hold for every input sequence within the bound:

Property	What it proves
No overflow	count ≤ DEPTH always
Flag consistency	empty ⇔ count=0, full ⇔ count=DEPTH
Pointer/count agreement	wr_ptr − rd_ptr ≡ count (mod DEPTH)
Data integrity	A solver-chosen word is read back unmodified, in order
Cover	FIFO can reach both full and empty

Inputs are driven with anyseq — the solver explores adversarial sequences, not a random sample.

3. Synthesis (make synth)

Confirms no simulation-only constructs slipped in. 352 cells — see docs/synth_report.txt.

Something I learned building this

The first formal run failed — not because the FIFO was wrong, but because the harness referenced dut.wr_ptr hierarchically and Yosys created undriven wires, giving the solver room to fabricate a counterexample.

Fix: keep internal invariants inside the module under `ifdef FORMAL, and let the external harness check only ports. That's the pattern I still use.

Separately, the scoreboard once reported 998 false errors from blocking/nonblocking sampling skew in the checker itself. Debugging your own TB is half of real DV work.

Layout

.
├── rtl/sync_fifo.v
├── tb/tb_sync_fifo.v
├── formal/fifo_props.sv · fifo.sby
├── docs/synth_report.txt
└── Makefile · .github/workflows/ci.yml

---

Portfolio · LinkedIn · GitHub