The symptom is a FIFO that lies about itself: full asserted with space left, empty asserted with data waiting, and eventually overflow or underflow corrupting the stream. The pointers look right in single-clock simulation because both sides see every update atomically; the failure needs the two clocks and the skew between pointer bits, which is exactly what unit simulation never provides.
The simulation output below crosses a 3-bit binary write pointer through per-bit synchronisers with deterministic per-bit skew, the honest model of wires with different delays. The pointer steps 3 to 4, changing all three bits at once.
How to read it: ptr is the source pointer stepping 1, 2, 3, 4, 5. q1 is the first synchroniser stage and sync the second. Single-bit steps cross cleanly, but the three-bit step from 3 to 4 tears: the first stage captures 7 and the second stage delivers 7, a value a one-step counter can never produce between 3 and 4, before settling to 4.
A binary pointer routinely changes several bits in one step, and each bit resolves independently in its own synchroniser, so the sampled pointer mixes old and new bits. Full and empty are computed by comparing the local pointer against the crossed one, so a torn sample manufactures a false full or a false empty. The damage compounds: a false empty reads stale data forward, a false full drops a write, and the stream is corrupt with no flag to say so.
Structural analysis expects Gray pointers on FIFO crossings and reports a binary pointer as a multi-bit crossing without a protocol. The Gray-pointers lesson of the async-FIFO topic states what the check looks for: a registered Gray value advancing one step at a time, synchronised bit by bit. Any pointer that can reload or skip breaks the one-bit discipline and needs a different structure, not Gray.
Fix it by crossing registered Gray pointers and converting back at the destination, with the full and empty logic written conservatively so each flag errs on its safe side. The guard is an assertion the design can carry forever: the sampled pointer must always equal the old or the new source value within the synchroniser latency, never a third value. That assertion fails on binary pointers the first time a multi-bit step aligns with a sampling edge, which is precisely the regression this bug needs.
A one-step counter between 3 and 4 can only ever hold 3 or 4; 7 matches neither, so it is a mix of old and new bits, not a timing offset.
With one clock both sides sample every pointer update atomically, so no torn sample can form. The tear needs two clocks plus skew between the pointer bits.