Check the FIFO rules while data moves
A stale full decision can allow one write too many. Concurrent traffic and independent pointer assertions expose the error.
Public demonstration
This is not a client result. The recorded command and check status appear below.
Recorded outcome
All seven correct workloads pass. The stale full comparator naturally passes two workloads that avoid full and fails the five that reach it. The complete matrix also checks the retained synchronizer and write-pointer negative controls.
What was checked
- Problem
- A data-transfer test may miss a pointer update or synchronizer pipeline error. The internal rules need checks that remain active during a regression.
- Scope
- A compact asynchronous FIFO using the classic Gray pointer design, at depths 4 and 8 and widths 5, 8, and 13. Seven workloads vary traffic, clock ratios, phase offsets, and deterministic seeds. This is demonstration RTL, not production IP.
- Approach
- A queue checks accepted data in order during concurrent writes and reads. Independent checks decode synchronized Gray pointers to derive full and empty expectations. A seeded stale-pointer comparison passes short and non-full traffic but fails workloads that reach full. Separate synchronizer and blocked-write controls remain in the matrix.
- Evidence
- The runner verifies the imported FIFO against its pinned public source hash, compiles with assertions enabled, and retains logs and durations. It rejects an incomplete matrix, timeouts, wrong negative-control diagnostics, and a passing marker accompanied by a failure.
Scope and limits
What these checks do not establish.
- This is compact demonstration RTL with synthetic defects, not a discovered production FIFO bug.
- Assertions are executed in digital simulation, not formal proofs or electrical CDC sign off.
- Only the stated configurations and finite traffic are checked. Reset is released in stages while idle; reset interruption during traffic is outside the matrix.
- Exercise counters are not complete code or functional coverage. Analog metastability and physical timing constraints are not modelled.
Reproduce and inspect
Recorded verification status
Revision 9cbdb40 was tested on 15 September 2026 with Verilator 5.050. Twelve builds and all 28 expected simulation outcomes match: seven correct runs, four required mutant passes, and seventeen specific mutant failures. Nine runner regressions pass.
git clone https://github.com/Rivoryxa-Technologies/fifo-assertion-verification
cd fifo-assertion-verification
# Requires Python 3, Verilator, make, and a C++ compiler.
make testrtl/async_fifo.svunchanged pinned demonstration FIFOtb/fifo_properties.svindependent pointer and flag assertionstb/tb.svconcurrent scoreboard and boundary stimulustools/run.pyexact matrix and evidence validationrecorded/2026-09-15-matrix/reviewed resultsWant this method on your design?
Share the problem in a few lines. We will discuss the scope before any confidential project material changes hands.
Discuss a verification problem