A production quality, parameterized asynchronous clock domain crossing (CDC) FIFO in SystemVerilog, taken end to end with a fully open source ASIC flow: clean RTL, layered verification with a scoreboard and formal proofs, a real IEEE 1801 UPF low power intent, and a 60 configuration power, performance, and area (PPA) sweep on the SkyWater Sky130 process. Everything reproduces from a clean checkout with a single command, and every number in the report is generated rather than typed by hand.
A CDC FIFO is one of the most common and most failure prone blocks in a system on chip: its pointers live in two unrelated clock domains, and moving them across the boundary without metastability is the whole problem. This project solves it with the standard Cummings scheme (binary pointers with an extra wrap bit, gray coded before the crossing, synchronized through a sweepable N flop chain) and then proves, measures, and documents the result.
- Parameterized RTL in clean SystemVerilog: data width, depth, and synchronizer depth are all parameters, with gray coded pointers, per domain reset synchronizers, and both fine grain and coarse grain clock gating.
- Layered verification: self checking unit tests, a randomized integration testbench with a SystemVerilog queue scoreboard across four clock ratio regimes, Verilator lint clean, and formal proofs in SymbiYosys of no overflow, no underflow, gray adjacency, and full and empty disambiguation.
- Real low power intent: an IEEE 1801 UPF file with four power domains, a switchable write domain, and isolation clamps, cross referenced against the elaborated design by a structural lint and exercised in simulation.
- A 60 configuration PPA sweep through Yosys and OpenSTA against Sky130, with area, timing slack, and power (assumed and VCD measured) extracted to CSV, plus an analytical mean time between failures analysis of the synchronizer depth trade.
- Reproducible by construction:
make setup && make allrebuilds every deliverable, the sweep regenerates a byte identical results file, and a style gate forbids stray dash characters across the whole tree, including the compiled PDFs.
Two compiled PDFs, viewable directly on GitHub:
- Main report: the design, the low power intent, the verification plan, the synthesis and timing methodology, and the full results.
- Engineering debug report: a first person postmortem of the real problems solved along the way, including a formal counterexample about full and empty flags in an asynchronous FIFO.
Two clock domains, joined only by the gray coded pointer synchronizers and the shared memory.
flowchart LR
subgraph WR[Write domain, wr_clk]
WP[write pointer<br/>full, almost_full]
WICG[write and RAM<br/>clock gates]
RS2W[read gray<br/>synchronizer]
ISO[isolation clamp<br/>retention]
end
subgraph MEM[Memory domain]
RAM[dual port RAM<br/>sync write, async read]
end
subgraph RD[Read domain, rd_clk]
RP[read pointer<br/>empty, almost_empty]
RDICG[read pointer<br/>clock gate]
WS2R[write gray<br/>synchronizer]
end
wr_data --> RAM
WP -- wr_addr --> RAM
RAM -- rd_data --> rd_data
RP -- rd_addr --> RAM
WP --> ISO --> WS2R --> RP
RP --> RS2W --> WP
See docs/architecture.md for the full microarchitecture and parameter table.
All figures below are generated from the sweep results file
(experiments/results/summary.csv) and are
regenerated by make report.
Area scales with depth times width, since the memory dominates. Adding a synchronizer stage adds only a handful of flip flops.
Small configurations meet the 10 ns timing target; the largest violate it as the read pointer fanout into the memory read multiplexer grows. This is a pre layout estimate, so the slack is pessimistic but consistent across the sweep.
Power rises with size, and the activity measured from a real workload VCD runs above the flat default assumption.
The synchronizer depth trade is the core low power study: each added stage costs a little area, a little power, and one cycle of latency, and buys a mean time between failures that improves roughly exponentially.
| Configuration | Cells | Area (um2) | WNS (ns) | Power (mW) |
|---|---|---|---|---|
| depth 4, width 8, sync 2 | 135 | 2426 | +2.84 | 0.52 |
| depth 16, width 32, sync 2 (default) | 869 | 21159 | +0.87 | 3.23 |
| depth 64, width 64, sync 2 | 7586 | 158058 | -46.25 | 11.80 |
| Level | What it checks | Result |
|---|---|---|
| Unit | gray codec, synchronizer, memory | 3 of 3 pass under Icarus |
| Integration | scoreboard, 4 clock ratio regimes, all sync depths | thousands of transfers, zero errors |
| Lint | Verilator -Wall, single top |
clean, one documented waiver |
| Formal | overflow, underflow, gray adjacency, mutual exclusion | proven, bounded, in SymbiYosys |
| Low power | UPF structural lint and gating and isolation simulation | pass |
Prerequisites: a Linux environment (WSL2 works), the OSS CAD Suite (Yosys,
Icarus, Verilator, SymbiYosys), OpenSTA built from source, the Sky130 PDK fetched
with ciel, and a TeX Live install for the reports. Exact versions are recorded
in PROGRESS.md.
make setup # python venv, dependencies, and the Sky130 PDK
make all # style, lint, sim, formal, UPF, synth, STA, the sweep, both PDFsIndividual stages are also available: make sim-unit, make sim-integration,
make formal, make upf-lint, make sim-power, make synth, make sta,
make sweep, and make report. Run make help for the full list.
On the development machine, replacing rough estimates with real numbers: the full 60 configuration sweep runs in about 13 seconds, the bounded formal proof in about 50 seconds, and the whole flow in a couple of minutes. The designs are small, so everything is well under an hour.
| Path | Contents |
|---|---|
rtl/ |
the FIFO and its parts |
tb/ |
unit and integration testbenches with the queue scoreboard |
formal/ |
the SymbiYosys harness and proofs |
upf/ |
the IEEE 1801 power intent and its structural lint |
syn/ |
the Yosys and OpenSTA scripts and constraints |
experiments/ |
the sweep, the results, and the MTBF model |
docs/ |
architecture, verification plan, UPF rationale, synthesis flow, results, and the engineering log |
report/, report_debug/ |
the two LaTeX reports |
assets/ |
figures and compiled PDFs for this page |
- Architecture
- Verification plan
- UPF power intent
- Synthesis flow
- Results summary
- Design decisions
- Engineering log
Released under the MIT License. See LICENSE.