Formal CDC Verification

Simulation finds bugs that were triggered. Formal CDC verification proves that no bug can exist — for every possible input sequence, every synchronizer correctly handles the crossing. This lesson covers the complete flow: static structural analysis with SpyGlass CDC, mathematical proof with JasperGold, SVA properties for CDC correctness, and the sign-off process that closes a design for tape-out.

1. Static vs Formal CDC — What Each Does

The two verification methods answer different questions and are used in sequence, not as alternatives.

Static CDC analysis is structural. It parses the RTL, identifies which clock drives each register, builds a clock domain graph, and then checks every signal that crosses a domain boundary. It answers: "Is there a synchronizer here? Is it the right type? Does the fanout create reconvergence?" Static tools are fast — they scale to hundreds of millions of gates — and they flag missing synchronizers within minutes of running.

Formal CDC verification is mathematical. It takes the synchronizer structure that static analysis found and proves — for all possible input sequences — that the synchronizer correctly isolates the two domains. It uses model checking: exploring the full state space of the synchronizer circuit and proving that no input sequence can cause a CDC violation. If it finds a sequence that violates the property, it produces a counterexample (CEX) — a concrete waveform showing exactly what must happen to trigger the bug.

2. What Static CDC Analysis Does

A static CDC tool performs the following steps automatically:

1. Clock tree extraction — identify every clock signal, its frequency, and which registers it drives
2. Domain assignment — assign each register to a clock domain; detect domains generated by muxes, dividers, or gating
3. Crossing point identification — find every combinational path where the driver is in domain A and the load is in domain B
4. Synchronizer check — verify each crossing has an appropriate synchronizer: 2-FF for single-bit, FIFO for multi-bit data, MCP for multi-cycle paths
5. Reconvergence analysis — trace synchronizer outputs for fanout that reconverges with unsynchronized logic from the source domain
6. Protocol check — for handshake crossings, verify the req/ack pair is complete and correctly ordered

3. Reconvergence Fanout (SRFF) — The Subtle CDC Bug

Reconvergence fanout is the most commonly missed CDC issue in static analysis. It is easy to construct a design where every crossing has a synchronizer, all synchronizers are correct, and yet the design still has a CDC bug.

Here is what happens: Signal sig_a originates in domain A. It crosses to domain B through a 2-FF synchronizer producing sig_b_sync. Good so far. But the designer then uses sig_a — the original, unsynchronized version — in combinational logic inside domain B, and the output of that combinational logic converges with sig_b_sync at a register in domain B.

At the convergence point, there are now two versions of the same signal: one delayed by one or two destination clock cycles (the synchronized copy) and one that may have already changed again (the source domain copy). The logic at the convergence point sees inconsistent values and produces corrupted output — even though every individual crossing had a synchronizer.

4. SpyGlass CDC Workflow

SpyGlass is Synopsys's industry-standard static CDC tool. The typical flow has four phases: read, compile, run goals, review results. The Tcl script below shows a complete production-ready setup.

## SpyGlass CDC Setup Script
## Phase 1: Read design files
read_file -type verilog {
    rtl/top.sv
    rtl/sync_2ff.sv
    rtl/cdc_fifo.sv
    rtl/clk_a_domain.sv
    rtl/clk_b_domain.sv
}

## Phase 2: Specify clocks and frequencies
set_option clock_domain {clk_a 200}    ;# 200 MHz
set_option clock_domain {clk_b 125}    ;# 125 MHz
set_option clock_domain {clk_ref 50}   ;# 50  MHz

## Specify asynchronous clock relationships
set_option async_clk_pairs {{clk_a clk_b} {clk_a clk_ref}}

## Phase 3: Set synchronizer recognition
## Tell SpyGlass what your 2-FF synchronizer cell is called
set_option sync_cell {sync_2ff}
set_option sync_depth 2

## Phase 4: Compile design
compile_design -top top_module

## Phase 5: Run CDC goal
current_goal {CDC/cdc_setup}
run_goal

## Run detailed analysis goals
current_goal {CDC/cdc_verify}
run_goal

## Generate reports
report_cdc -file cdc_violations.rpt -type violations
report_cdc -file cdc_waivers.rpt   -type waivers
report_cdc -file cdc_summary.rpt   -type summary

After running, SpyGlass produces a violation list. Each entry shows the crossing signal, the source domain, the destination domain, the rule that fired, and a severity level (error, warning, info). Engineers must disposition each violation — either fix it (add or correct the synchronizer) or waive it with documented justification.

## SpyGlass CDC Waiver File
## Format: waive -rule RULE_NAME -signal SIGNAL_PATH -comment "justification"

## Waiver 1: False path -- signal is stable when sampled
## SDC contains set_false_path from clk_a domain
## to cfg_mode_b register; only changes during reset
waive -rule Ac_unsync01 \
      -signal {top.u_ctrl.cfg_mode} \
      -comment "False path per SDC: cfg_mode only changes \
                during global reset; guaranteed stable \
                before clk_b domain samples it"

## Waiver 2: Gray-code counter -- tool cannot prove 1-bit
## change statically; our encoding guarantees it
waive -rule Ac_unsync04 \
      -signal {top.u_fifo.wr_ptr[3:0]} \
      -comment "Gray-code encoded write pointer; \
                only 1 bit changes per cycle by design; \
                verified by formal proof in jasper run 2026-06-23"

## Waiver 3: Reset synchronizer topology not recognized
waive -rule Ac_reset01 \
      -signal {top.u_rstsync.rst_b_sync} \
      -comment "Reset synchronizer at u_rstsync uses \
                async assert / sync deassert topology; \
                SpyGlass does not recognize this cell; \
                cell reviewed and approved by CDC lead"

5. Formal CDC with JasperGold CDC App

JasperGold's CDC App automates the formal verification of synchronizer correctness. It does not require you to write properties manually for straightforward synchronizers — the tool auto-extracts prove targets. You only write manual SVA for protocol-level properties (handshake ordering, gray-code monotonicity, FIFO pointer ordering).

The CDC App works in three steps:

1. Abstraction — the tool reads the RTL and automatically identifies synchronizer structures from the clock domain graph
2. Property generation — for each synchronizer, it generates prove targets: "the output of this synchronizer must be stable when sampled by the destination clock"
3. Proof / CEX — model checking runs on each prove target; if all pass, the synchronizer is formally verified; if any fail, a CEX waveform is generated showing exactly which input sequence triggers the failure

## JasperGold CDC App Tcl Script

## Step 1: Elaborate design
analyze -sv09 {
    rtl/top.sv
    rtl/sync_2ff.sv
    rtl/cdc_fifo.sv
    rtl/clk_a_domain.sv
    rtl/clk_b_domain.sv
}
elaborate -top top_module

## Step 2: Define clocks
clock clk_a -period 5     ;# 200 MHz (5 ns period)
clock clk_b -period 8     ;# 125 MHz (8 ns period)
clock clk_ref -period 20  ;# 50  MHz (20 ns period)

## Step 3: Define resets
reset -expression {!rst_n}

## Step 4: Load CDC App -- auto-generates prove targets
cdc run

## Step 5: Review CDC app results
cdc report -severity {error warning} \
           -file cdc_formal_report.rpt

## Step 6: Add manual assume/guarantee for protocol properties
## Constrain the source domain input behavior
assume -name A_REQ_STABLE {
    @(posedge clk_a) $stable(req) |-> ##[1:2] $stable(req)
}

## Prove handshake property on destination side
prove -name P_ACK_AFTER_REQ {
    @(posedge clk_b) req_sync |-> ##[1:4] ack
}

## Step 7: Run formal engine on all targets
prove -all

## Step 8: Generate closure report
cdc report -type closure -file cdc_closure.rpt

6. Assume-Guarantee for CDC

Formal CDC at the full-chip level can be computationally intractable because the state space of two fully independent clock domains is enormous. The industry solution is assume-guarantee (AG) decomposition — splitting the proof into sub-problems that each run on a manageable piece of the design.

The key idea: when proving domain B's synchronizer, you do not need to model the full behavior of domain A. Instead, you write an assumption that constrains what domain A inputs look like at the domain boundary. Then you prove that if those assumptions hold, domain B's synchronizer output is always valid.

To compose proofs hierarchically:

1. Prove domain A produces outputs that satisfy the assumption constraints
2. Prove domain B's synchronizer is correct given those constrained inputs
3. Chain the proofs: since A satisfies the assumptions and B is correct under those assumptions, the composed system is mathematically correct

// Assume-Guarantee CDC Properties
// File: cdc_ag_properties.sv

module cdc_ag_props (
    input logic clk_a, clk_b, rst_n,
    input logic sig_a,          // source domain signal
    input logic sig_b_sync,     // synchronized output in domain B
    input logic sig_b_sync_q    // one cycle delayed in domain B
);

  // -------------------------------------------------------
  // ASSUMPTIONS -- constrain domain A behavior at boundary
  // -------------------------------------------------------

  // A1: sig_a must remain stable for at least 3 clk_a cycles
  //     before any transition (meets 2-FF synchronizer setup)
  property A_SIG_STABILITY;
    @(posedge clk_a) disable iff (!rst_n)
    $changed(sig_a) |-> $past($stable(sig_a), 3);
  endproperty
  assume property (A_SIG_STABILITY);

  // A2: No glitches -- sig_a cannot pulse for less than 1 cycle
  property A_NO_GLITCH;
    @(posedge clk_a) disable iff (!rst_n)
    $rose(sig_a) |-> sig_a ##1 sig_a;
  endproperty
  assume property (A_NO_GLITCH);

  // -------------------------------------------------------
  // GUARANTEES -- prove domain B synchronizer correctness
  // -------------------------------------------------------

  // G1: Synchronizer output must never be X
  property G_SYNC_STABILITY;
    @(posedge clk_b) disable iff (!rst_n)
    !$isunknown(sig_b_sync);
  endproperty
  prove_property: assert property (G_SYNC_STABILITY);

  // G2: Synchronizer output must eventually track source
  //     (liveness -- no permanent de-sync)
  property G_SYNC_LIVENESS;
    @(posedge clk_b) disable iff (!rst_n)
    $rose(sig_a) |-> ##[2:6] sig_b_sync;
  endproperty
  prove_liveness: assert property (G_SYNC_LIVENESS);

  // G3: Safety -- synchronized output never contradicts
  //     source while source is in steady state
  property G_NO_CONTRADICTION;
    @(posedge clk_b) disable iff (!rst_n)
    ($stable(sig_a) && !sig_a) |-> ##[0:4] !sig_b_sync;
  endproperty
  prove_safety: assert property (G_NO_CONTRADICTION);

endmodule

7. Key CDC Formal Properties (SVA)

Beyond the auto-generated synchronizer proofs, CDC sign-off requires manually written SVA properties for protocol-level guarantees. The four most critical categories are:

// Async FIFO CDC SVA Properties

module fifo_cdc_props #(parameter DEPTH = 8, AW = 3) (
    input logic clk_wr, clk_rd, rst_n,
    input logic [AW:0] wr_ptr_gray, rd_ptr_gray,
    input logic [AW:0] wr_ptr_bin,  rd_ptr_bin,
    input logic wr_en, rd_en,
    input logic full, empty
);

  // Gray-code monotonicity -- exactly 1 bit changes per write clock
  property P_GRAY_MONOTONE;
    @(posedge clk_wr) disable iff (!rst_n)
    $changed(wr_ptr_gray) |->
      $onehot(wr_ptr_gray ^ $past(wr_ptr_gray));
  endproperty
  gray_monotone: assert property (P_GRAY_MONOTONE);

  // Full flag: write pointer has lapped read pointer by DEPTH
  property P_FULL_CORRECT;
    @(posedge clk_wr) disable iff (!rst_n)
    full == (wr_ptr_bin - rd_ptr_bin == DEPTH);
  endproperty
  full_correct: assert property (P_FULL_CORRECT);

  // Empty flag: pointers are equal
  property P_EMPTY_CORRECT;
    @(posedge clk_rd) disable iff (!rst_n)
    empty == (wr_ptr_bin == rd_ptr_bin);
  endproperty
  empty_correct: assert property (P_EMPTY_CORRECT);

  // No write when full (no overflow)
  property P_NO_OVERFLOW;
    @(posedge clk_wr) disable iff (!rst_n)
    full |-> !wr_en;
  endproperty
  no_overflow: assert property (P_NO_OVERFLOW);

  // No read when empty (no underflow)
  property P_NO_UNDERFLOW;
    @(posedge clk_rd) disable iff (!rst_n)
    empty |-> !rd_en;
  endproperty
  no_underflow: assert property (P_NO_UNDERFLOW);

endmodule

8. False Positives in Static CDC Analysis

Static CDC tools produce false positives — violations that are structurally flagged but are not real bugs. Understanding when a waiver is legitimate versus when it is hiding a real problem is a critical CDC engineering skill.

Legitimate waiver categories:

• SDC false paths — a signal that only changes during reset or configuration mode, documented in the SDC with set_false_path, and guaranteed stable when any destination clock samples it. The tool cannot read SDC semantics so it flags the crossing even though it is safe by design intent.
• Unrecognized synchronizer topology — your company's custom synchronizer cell uses a specific flop instantiation that SpyGlass does not recognize from its cell library. The synchronizer is correct; the tool just does not know the cell name.
• Gray-code counters — static analysis cannot statically prove that a counter encoding guarantees single-bit transitions; it sees a multi-bit bus crossing and flags it. With formal proof of the gray-code property, the waiver is justified.
• Constant signals — signals tied to constant values in specific configurations are flagged as CDC crossings even though they can never change and are therefore safe.

9. CDC Sign-off Flow

CDC sign-off is a formal gate in the tape-out checklist. The closure process has six steps that must be completed in order:

1. Static CDC clean — run SpyGlass CDC with all goals; all errors must be either fixed in RTL or waived with approved written justification
2. Waiver review — design lead and verification lead jointly review every waiver; any questionable waiver escalates to the chip architect
3. Formal proof — run JasperGold CDC App on all crossing clusters; all auto-generated prove targets must return PROVEN; any CEX result requires RTL fix and re-run
4. Protocol properties — run manual SVA properties (handshake ordering, gray-code monotonicity, FIFO pointers) to PROVEN state
5. CDC closure report — generate a report listing: total crossings found, number fixed, number waived (with justification index), number formally proven
6. Sign-off approval — DV lead, CDC lead, and physical design lead sign the closure report; the block is gated for tape-out

10. Questa CDC — Comparison to SpyGlass

Siemens Questa CDC (formerly part of ModelSim) provides a similar structural analysis capability to SpyGlass with different rule naming and a GUI-focused waiver manager. Both tools share the same fundamental approach; knowing one transfers directly to the other.

## Questa CDC Run Script

## Read design
vlog -sv rtl/top.sv rtl/sync_2ff.sv rtl/cdc_fifo.sv

## Define CDC intent
cdc run -d top_module \
        -clock clk_a -period 5 \
        -clock clk_b -period 8 \
        -async_pairs {{clk_a clk_b}} \
        -output_dir questa_cdc_results

## Load synchronizer recognition library
cdc prefer_sync_cell -cell sync_2ff -depth 2

## Run full CDC analysis
cdc analyze

## Generate reports
cdc report violations -file questa_violations.rpt
cdc report waivers    -file questa_waivers.rpt
cdc report summary    -file questa_summary.rpt

## Launch interactive GUI for waiver management
## questa_cdc_gui questa_cdc_results/cdc_db

FAQ

← Full course roadmap