cdc-verification-lib

Clock-domain-crossing primitives in SystemVerilog, each shipping with the formal proof of its own safety contract - plus dual-clock cocotb regressions that exercise the same modules across unrelated clock rates.

CDC bugs do not show up as failing tests; they show up as a board that works on the bench and corrupts data in the field. That makes CDC one of the few areas where formal verification is not a luxury - the properties are small, provable, and worth proving. Every module here carries its properties inside the source under `ifdef FORMAL, so a user can re-prove them in their own flow rather than trusting a claim.

Modules

Module	Crossing	Proved contract
sync_2ff	1 bit, level	Output is always a delayed copy of a real input sample; a value held for two cycles is guaranteed to appear
pulse_sync	single-cycle pulses	Every destination pulse corresponds to exactly one toggle edge; src_busy marks the in-flight window that makes pulse loss impossible
handshake_sync	N-bit word	The committed word is stable for the entire request; four-phase req/ack ordering; delivered data equals the committed word
async_fifo	streams (Gray pointers)	Gray pointers change by exactly one bit; occupancy never exceeds depth; full/empty actually protect the storage

Formal verification

cd formal
sby -f sync_2ff.sby        # PASS (unbounded proof)
sby -f pulse_sync.sby      # PASS (unbounded proof)
sby -f handshake_sync.sby  # PASS (unbounded proof)
sby -f async_fifo.sby      # PASS (BMC, depth 40)

Requires the open OSS CAD Suite (Yosys + SymbiYosys + Z3) - no commercial licence involved.

Honest scoping, since formal claims are easy to overstate:

• The synchronizer, pulse and handshake modules are proved by unbounded temporal induction - the properties hold for all reachable states.
• The FIFO is checked by bounded model checking to depth 40, which covers wrap-around of both pointers on the depth-8 configuration. Full induction on a two-pointer FIFO needs a large set of auxiliary invariants relating the stale synchronized pointers to the true ones; that is a known hard case and is left as future work rather than papered over.
• Proofs run in a single-clock abstraction (both domains tied to one formal clock). This is deliberate: it proves the logical CDC contracts - Gray transitions, handshake ordering, data stability, flag protection. The metastability window itself is handled by the 2-FF structures and ASYNC_REG attributes, not by a solver.
• The f_* wrappers in formal/f_wrappers.sv drive only what the contract requires (e.g. no pulse while src_busy); every other input is left free for the solver to attack.

Simulation

python tb/run.py            # requires iverilog + cocotb

The cocotb suites run the modules with genuinely unrelated clock periods (7 ns vs 11.3 ns, 13.7 ns vs 5 ns, 8 ns vs 12.7 ns, 6 ns vs 17.3 ns) and random stalls on both sides, checking end-to-end integrity: every word and pulse arrives exactly once, in order.

fifo        TESTS=2 PASS=2   (fast-writer and fast-reader directions, 400 words each)
handshake   TESTS=1 PASS=1   (60 words)
pulse       TESTS=1 PASS=1   (50 pulses)
sync_2ff    TESTS=1 PASS=1   (smoke test alongside the unbounded proof)

Using these in a design

Instantiate directly, or lift the `ifdef FORMAL blocks as a checklist for reviewing an existing crossing. The two questions worth asking of any CDC in a code review are the ones these proofs encode: what is the stability contract on the data, and what happens when the source moves faster than the destination can observe.

License

MIT