Formal Verification for CDC

1. Why Formal Verification for CDC?

Simulation can only test a finite number of scenarios. Metastability bugs are probabilistic—they might occur 1 in 10 billion times, making simulation insufficient.

Formal verification proves properties mathematically, covering ALL possible execution traces.

For CDC, formal verification answers critical questions:

• ✅ Is MTBF > 1 million years? (Not just simulated, but proven)
• ✅ Can FIFO ever deadlock? (Proven impossible)
• ✅ Will data ever be lost or corrupted? (Proven to never happen)
• ✅ Are setup/hold ever violated in non-metastable regimes? (Proven no)

2. Formal Specification: Properties in Temporal Logic

LTL (Linear Temporal Logic)

Express CDC properties in LTL syntax:

3. Formal CDC Verification Approaches

Model Checking

The formal tool builds a state machine from the RTL and exhaustively verifies all reachable states against the properties.

For a 256-entry FIFO with 8-bit write_ptr and 8-bit read_ptr, the state space is 2^16 ≈ 65,000 states. Manageable for model checkers.

Tools: Cadence IUS, Mentor Questa, OneSpin, Jasper Gold

Theorem Proving

For larger designs, theorem provers use mathematical logic to prove properties without exhaustive state exploration.

Tools: ACL2, Isabelle/HOL, Coq

4. MTBF Formal Verification

Proving Exponential Decay

Formal verification can prove the exponential metastability decay formula:

// Formal property for MTBF in PSL (Property Specification Language)
// Used in Mentor Questa or Cadence tools

// Define metastable state (FF1 output between V_IL and V_IH)
metastable_ff1 = (ff1_out > V_IL) & (ff1_out < V_IH);

// Define resolved state (FF1 output clearly 0 or 1)
resolved_ff1 = (ff1_out <= V_IL) | (ff1_out >= V_IH);

// Property: Exponential resolution
// "If metastable at clock edge T, will resolve within Δt with probability P(τ, Δt)"
assert always (
  (metastable_ff1 && @ CLOCK_A_EDGE)
  -> (F[<=N_CYCLES] resolved_ff1)
);

// Property: Dual-FF MTBF exponential safety
// "Probability of FF2 capturing metastability decays exponentially"
assert always (
  metastable_ff1_at_T
  -> P(fail_ff2) < exp(-τ * Δt)
);

// Result: Formal proof that MTBF(two-stage) > 1 million years

5. Formal CDC Lint Tools

CDC lint tools automatically check for common violations:

Lint tools integrate with design flow: Run after simulation, before layout. Typical pass rate: CDC lint must pass with zero warnings before tape-out.

6. Formal Verification Workflow

Step 1: Write properties in LTL/PSL describing expected CDC behavior

Step 2: Configure assumptions about clock domains (no clock jitter, setup/hold met except in metastable window)

Step 3: Run formal proof (model checker exhausts state space or theorem prover constructs proof)

Step 4: Review counterexamples if property fails (indicates design bug)

Step 5: Fix design or property (either correct the CDC or refine the specification)

Step 6: Formal verification pass (all properties proven, ready for production)

7. Common Formal CDC Bugs Caught

• ❌ Missing synchronizers: Formal proof fails for "data consistency" property → reveals unsynchronized signal
• ❌ Insufficient stages: "MTBF > 1 year" property fails with single-FF → forces use of dual-FF
• ❌ Wrong encoding: Binary multi-bit crossing without Gray code → property "no glitches" fails
• ❌ Combinational cross-domain paths: "No combinational delay from Clock A to Clock B" fails → reveals async combinational logic
• ❌ Reset sync missing: "All resets synchronized" property fails → forces async reset synchronization

8. Formal vs. Simulation Trade-offs

Recommendation: Use both. Simulation for fast iteration, formal verification for production sign-off.

9. Formal Verification Best Practices

• ✅ Start early: Write properties while designing, not as afterthought
• ✅ Be specific: Properties must be unambiguous (avoid vague statements)
• ✅ Prove critical properties: Focus on MTBF, data integrity, no deadlock
• ✅ Bound time: Properties should have explicit time bounds (e.g., "within 100 cycles")
• ✅ Review counterexamples: If proof fails, counterexample shows the execution path leading to failure
• ✅ Version control:**properties like code—track changes, review sign-off