Synchronous FIFO — Formal Verification

A parameterized synchronous FIFO verified using SymbiYosys + Z3 SMT solver.

Design

• Parameterized DATA_WIDTH and DEPTH (default 8-bit × 16-deep)
• Extra-bit pointer method for full/empty disambiguation
• Active-low async reset (rst_n)
• count output tracks occupancy in real time

Properties Proved (k-induction)

1. On reset: empty=1, full=0, count=0
2. full and empty never simultaneously high
3. count always in range [0, DEPTH]
4. full iff count == DEPTH
5. empty iff count == 0
6. No overflow — write ignored when full
7. No underflow — read ignored when empty
8. Count increments by 1 on write-only (not full)
9. Count decrements by 1 on read-only (not empty)
10. Count stable on simultaneous valid read + write

Cover Points (Reachability)

• FIFO reaches full state
• FIFO drains from non-empty to empty
• FIFO reaches half-full (count == DEPTH/2)

Repository Structure

fv-fifo/

├── fifo.sv # RTL + formal properties (ifdef FORMAL)

├── fifo.sby # SymbiYosys configuration

└── README.md

How to Run

sby -f fifo.sby

Expected: DONE (PASS, rc=0)

Tools

• SymbiYosys — formal verification front-end
• Z3 — SMT solver backend
• OSS CAD Suite