Module 7 — Clock Domain Crossing

Verify asynchronous crossings formally. Model metastability with anyseq, prove what a two-flip-flop synchronizer really guarantees, and check a multi-bit handshake CDC.

Katas in this module (3)

• Kata 7.1 — The Missing Synchronizer
• Kata 7.2 — The Counter That Lost a Bit
• Kata 7.3 — Handshake CDC, Verified

Part of Hardware Formal Verification on formal.org.