Case study · Clock domain crossing
Proving a dual-clock FIFO safe
Assertion-based verification of a parameterized dual-clock asynchronous FIFO: Gray-code pointers, two-flop synchronizers, and an SVA suite regressed across five clock ratios on Cadence Xcelium.
- 14assertions
- 8cover properties
- 5clock-ratio scenarios
The problem: two clocks that never agree
When the write side and the read side of a FIFO run on unrelated clocks, each side still has to know where the other's pointer is. Sample a multi-bit binary pointer while it's changing and you can capture a value it never actually held: going from 7 to 8 flips four bits at once.
The standard fix, and the design here: keep binary pointers for addressing, cross Gray-coded pointers (only one bit changes per step) through two-flop synchronizers, and compute FULL in the write domain and EMPTY in the read domain.
The design
| Module | Role |
|---|---|
top.sv | Integration; enforces a power-of-two DEPTH at elaboration with $fatal, since the FULL/EMPTY comparison depends on it |
fifo_mem.sv | Memory array, written on w_clk and read on r_clk |
wfull.sv | Binary and Gray write pointers; FULL via the MSB-invert comparison |
rempty.sv | Binary and Gray read pointers; EMPTY detection |
sync_w2r.sv, sync_r2w.sv | Two-flop synchronizers, one per pointer crossing |
Assertions, bound from the outside
The checkers live outside the RTL and are attached with bind, so every design file still compiles for synthesis unchanged while the assertions reach internal signals no port exposes, like the Gray pointers and the first stage inside each synchronizer. Each property is clocked in the domain that owns its signals.
| Assertion | What it proves |
|---|---|
a_wptr_gray, a_rptr_gray | Each pointer changes by at most one bit per clock. The whole CDC scheme depends on this. |
a_no_overflow | A write while FULL never advances the write pointer, so unread data is never overwritten. |
a_no_underflow | A read while EMPTY never advances the read pointer. |
a_not_full_and_empty | FULL and EMPTY are never asserted together. |
a_reset_empty, a_reset_not_full | Reset leaves the FIFO empty, not full. |
a_stage1, a_stage2 | Each synchronizer really is two flops deep, stage by stage. |
a_two_flop_latency | Crossing latency is exactly two destination clocks: not fewer, not more. |
a_no_x_* | No X on the flags, the pointers, or read data during an active read. |
The 8 cover properties record that the interesting corners were actually reached, including FULL, EMPTY, write-while-full, read-while-empty, simultaneous read and write, and both flags releasing again.
Five clock ratios
| Scenario | Write : read half-period | Purpose |
|---|---|---|
| Balanced 1:1 | 5.0 : 5.0 ns | Baseline random traffic |
| Fast write, slow read | 5.0 : 15.0 ns | Drives the FULL boundary |
| Slow write, fast read | 15.0 : 5.0 ns | Drives the EMPTY boundary |
| Non-harmonic phase drift | 5.0 : 3.5 ns | Edge alignment drifts continuously, sweeping every phase relationship |
| FULL boundary hammer | 5.0 : 25.0 ns | Sustained backpressure against FULL |
Monitors sample through clocking blocks with input #1step, so the checker sees exactly what the DUT's flops acted on and can never race a non-blocking update. A reference queue catches both corrupted data and reordering.
What the first real Xcelium run caught
Testbench race
A write that slipped in during the drain
One shared enable drove both stimulus generators. At the switch from traffic to drain, the write generator could read the old write rate on the same clock edge the drain started (two processes woken by the same edge have no guaranteed order in SystemVerilog), sneaking in one extra write after the drain check had begun trusting the model. Reads were then cut off as soon as that check passed, stranding the write: “1 written item never came back out” in the slow-write, fast-read scenario.
Fix: separate write and read enables. Writes stop first, with a two-cycle settle on the write clock, and reads stay live for the whole drain, guaranteeing a lossless drain.
Wrong assertion
When the checker, not the design, was wrong
An early property asserted that the synchronized pointer changes by at most one bit per destination clock. That only holds when both clocks run at the same rate, so it fired on every non-1:1 scenario, while the scoreboard's independent data check stayed at zero mismatches. That disagreement pointed at the assertion, not the design: the one-bit-per-clock check belongs on each pointer's own clock, where it already existed.
A pass has to be earned
- Any data mismatch, underflow, data left behind after the drain, assertion failure or timeout fails the run.
- So does a run that saw no traffic, or never reached FULL or EMPTY. An untested corner is not a passing corner.
The concept, explained
Clock domain crossing
Async FIFO Explained: Gray Code, Synchronizers and the Full-Flag Twist
Builds an asynchronous FIFO step by step: the lap bit, metastability and the two-flop synchronizer, why a binary pointer going from 7 to 8 can arrive as 15, and how Gray code fixes it.