CDC Verification

1. Static vs Dynamic CDC Verification

Every CDC verification plan needs two independent layers. Neither alone is sufficient for tape-out sign-off, and the failure modes they catch are almost non-overlapping.

Static CDC analysis examines the RTL or gate-level netlist without executing a single simulation cycle. The tool (SpyGlass CDC, Questa CDC, JasperGold CDC) traverses the design graph, labels every flip-flop with its clock domain, and then inspects each signal that crosses from one domain to another. It checks: is there a recognized synchroniser structure on the crossing path? Does the synchroniser have the correct number of stages? Does the synchronised output fan out only to a single capture flop, or does it reconverge (SRFF)? Are multi-bit buses protected by a handshake or encoded as gray code? Static analysis produces a comprehensive report of every crossing — often hundreds in a real SoC — without needing test vectors.

Dynamic CDC verification runs simulation with metastability injection. Because simulation tools model flip-flops as ideal, a standard testbench will never produce a metastable output on a synchroniser — the DUT simply sees a clean 0 or 1. Metastability injection artificially adds a random resolution delay on each crossing signal so that the synchroniser may present either valid state to downstream logic. The simulation then checks that the design is functionally correct regardless of which value the synchroniser resolved to.

2. SpyGlass / Questa CDC Tool Flow

The industry CDC lint flow is a three-phase funnel: lint, structural CDC, then functional CDC. Each phase produces a categorised report and a waiver database. You carry forward only the residual violations that cannot be automatically fixed.

SpyGlass CDC Invocation (Tcl snippet)

## spyglass_cdc.tcl — minimal CDC run script
## Run with: spyglass -project cdc_run.prj -goal cdc_verify

# 1. Read design
read_file -type verilog {rtl/top.v rtl/sync_2ff.v rtl/fifo_async.v}
set_option top MyChip

# 2. Declare clocks
define_clock -name clk_a -period 5000  [get_ports clk_a]   ; # 200 MHz
define_clock -name clk_b -period 6666  [get_ports clk_b]   ; # 150 MHz
define_clock -name clk_c -period 10000 [get_ports clk_c]   ; # 100 MHz

# 3. Define recognised synchroniser cells
set_cdc_synchronizer -type FF2 sync_2ff ; # 2-flop sync
set_cdc_synchronizer -type PULSE pulse_sync ; # pulse sync

# 4. Classify crossings to ignore (resets, tied-off signals)
set_constant scan_mode 0

# 5. Run CDC goal
current_goal cdc_verify
run_goal

# 6. Report
write_report cdc_report.html

Questa CDC Lint Invocation

## questa_cdc.do — run from Questa CDC shell

cdc_run \
  -d MyChip \
  -work work \
  -src {rtl/top.sv rtl/sync_2ff.sv rtl/fifo_async.sv} \
  -clock {{clk_a -period 5ns} {clk_b -period 6.666ns}} \
  -cdc_report cdc_results/

# Check output
# cdc_results/cdc_summary.rpt — violation counts per category
# cdc_results/cdc_detail.rpt  — per-crossing path details
# cdc_results/cdc_srff.rpt    — SRFF candidates

3. Synchroniser Reconvergence Fanout (SRFF) Violations

SRFF (Synchroniser Reconvergence Fanout) is flagged when a synchroniser output fans out to multiple flip-flops or logic cones in the destination domain that later reconverge at a common gate. The CDC tool traces every load of the synchroniser's Q output and reports reconvergence whenever two paths from the same synchronised bit meet at an AND, OR, MUX, or any downstream flop whose inputs come from both paths.

SRFF is flagged as a potential violation because, in theory, a downstream reconvergence point could compare two different values derived from the same metastable bit — but in practice that cannot happen with a proper 2-FF synchroniser because both loads see the resolved (post-metastability) Q2 output. The real risk SRFF flags is a design topology where someone mistakenly placed logic between FF1 and FF2 in the synchroniser chain, or tapped off the partially-synchronised FF1 output for a faster but unsynchronised path.

SRFF Resolution Flow

1. Identify the tapped node. Look at the CDC report path — is the fanout coming from FF1 (first sync stage, partially synchronised) or FF2 (fully synchronised)? Fanout from FF1 is a real violation. Fanout from FF2 is usually false.
2. Check reconvergence function. If both paths from FF2-Q feed into a MUX with separate select lines, they are functionally independent and the SRFF is a false positive. Document this in the waiver.
3. Fix genuine SRFF. Re-structure the destination logic so the synchroniser output drives a single destination register first, then fan out from that registered version. This adds one cycle of latency but eliminates the reconvergence.
4. Waive false positives. For each waived SRFF, the waiver must state the signal name, source and destination modules, why reconvergence is safe (e.g., "both loads are read-only status registers and never combinationally reconverge").

4. Metastability Injection in Simulation

Simulation tools model flip-flops as ideal: if a signal changes too close to the clock edge, the simulator picks 0 or 1 deterministically (usually retaining the old value or picking the new one based on ordering). Metastability — the actual silicon failure mode where the flop output oscillates for nanoseconds before resolving — never appears in RTL simulation. Metastability injection bridges this gap artificially.

Random Delay Model

The most common approach inserts a random sub-cycle delay on every CDC crossing signal before it reaches the synchroniser's input. The delay is sampled from a uniform distribution over 0 to just under one destination clock period. At the extreme end of the delay range, the signal arrives just before the clock edge, mimicking the worst-case metastability window. Because the synchroniser resolves to 0 or 1 based on which cycle the delayed signal reaches, the functional effect is that the synchroniser resolves to either valid state with equal probability.

// =============================================================
// Metastability injection module — wraps a single CDC crossing
// signal. Insert one instance per crossing in the testbench.
// =============================================================
module meta_inject #(
  parameter int MAX_DELAY_PS = 5000   // max delay = just under dest period
) (
  input  logic clk_src,
  input  logic data_in,
  output logic data_out
);

real delay_ps;
logic data_delayed;

// Sample a new random delay on every source-clock rising edge
always @(posedge clk_src) begin
  delay_ps = $urandom_range(0, MAX_DELAY_PS);
end

// Apply the fractional delay to any transition on data_in
always @(data_in) begin
  // Non-blocking with a time delay in ps
  data_delayed <= #(delay_ps * 1e-12) data_in;
end

assign data_out = data_delayed;

endmodule

X-Injection Model

A complementary technique forces the crossing wire to 'X for a brief window after the source flop changes, then resolves to a randomly-chosen 0 or 1. The advantage is that any logic that combinationally uses the X will propagate X downstream, making metastability escapes immediately visible as X on primary outputs or memory write enables. Many simulators support this natively via the $X_inject PLI call or a UPF-based model.

// X-injection wrapper — simpler alternative to delay model
module x_inject (
  input  logic data_in,
  output logic data_out
);

always @(data_in) begin
  data_out = 1'bx;          // force X immediately on transition
  #100ps;                    // metastability resolution window
  data_out = $urandom[0];   // resolve to random 0 or 1
end

endmodule

5. SVA for Synchroniser Output Stability

After metastability injection, the synchroniser output must remain stable for at least two destination-clock cycles before being sampled by downstream logic. This is the fundamental property that makes a 2-FF synchroniser safe: the second flop samples the output of the first only after a full destination clock period, which is enough time for the first flop to resolve from metastability before the next capture edge.

We can verify this property directly in SVA. The key assertion checks that the synchroniser's second-stage output data_d (the value that downstream logic actually sees) does not change on consecutive clock edges of the destination clock. In other words, once data_d takes a new value, it must hold that value for at least two consecutive clk_b cycles.

// -------------------------------------------------------
// SVA: synchroniser output must be stable for >= 2 cycles
// after any transition on the destination-domain output.
// Bind this module to your 2-FF synchroniser instance.
// -------------------------------------------------------
module sync_sva (
  input logic clk_b,
  input logic rst_b_n,
  input logic data_d   // FF2 output — what dest logic sees
);

`ifdef FORMAL_OR_SIM_ASSERTIONS

// Property: after data_d changes, it must hold the same value
// on the very next clock edge (i.e., no glitch on consecutive cycles)
property p_sync_stable;
  @(posedge clk_b) disable iff (!rst_b_n)
  $changed(data_d) |=> $stable(data_d);
endproperty

assert property (p_sync_stable)
  else $error("[CDC] Synchroniser output changed on back-to-back cycles — metastability escape?");

// Cover: synchroniser output does eventually transition (sanity check)
cover property (@(posedge clk_b) $rose(data_d));
cover property (@(posedge clk_b) $fell(data_d));

`endif

endmodule

// Bind to every 2-FF synchroniser instance in the design:
bind sync_2ff sync_sva u_sync_sva (
  .clk_b   (clk_dest),
  .rst_b_n (rst_n),
  .data_d  (q2)
);

The $changed(data_d) |=> $stable(data_d) construct reads: "if data_d changed on this clock edge, then on the immediately following clock edge it must remain the same." A violation of this property during simulation with metastability injection is evidence of a real metastability escape — the X resolved to different values on two successive samples, implying the first-stage flop was still resolving when the second stage captured it. This is a critical design bug requiring either a longer synchroniser chain (3-FF) or a reduced clock frequency.

6. Gray Code Pointer Verification

Asynchronous FIFOs use gray-coded read and write pointers specifically to ensure that only one bit changes per pointer increment. This property is essential for safe CDC: when the gray-coded pointer crosses from the write clock domain to the read clock domain (or vice versa), the synchroniser may sample it during a transition — but since only one bit changes at a time, the worst case is that the destination domain sees either the old value or the new value, never a third, invalid pointer value.

If the gray code encoding is wrong — or if the binary-to-gray conversion has a bug — then two or more bits may change simultaneously on a pointer increment, and the synchroniser may capture an illegal intermediate state that does not correspond to any valid FIFO depth. This is the root cause of the classic async FIFO metastability bug.

SVA: Only One Bit Changes Per Pointer Step

// -------------------------------------------------------
// SVA: Gray code pointer must change by exactly 1 bit
// per clock cycle (including wrap-around at FIFO boundary).
// Apply this to both write pointer and read pointer.
// -------------------------------------------------------
module gray_ptr_sva #(
  parameter int PTR_W = 4   // pointer width in bits
) (
  input logic             clk,
  input logic             rst_n,
  input logic [PTR_W-1:0] gray_ptr
);

`ifdef FORMAL_OR_SIM_ASSERTIONS

// Only one bit must change per step after reset
property p_gray_onehot_change;
  @(posedge clk) disable iff (!rst_n)
  $changed(gray_ptr) |->
    $onehot(gray_ptr ^ $past(gray_ptr));
endproperty

assert property (p_gray_onehot_change)
  else $error("[GRAY] Pointer changed by != 1 bit: was 0x%0h, now 0x%0h",
              $past(gray_ptr), gray_ptr);

// Pointer must not be all-X after reset de-asserts
assert property (@(posedge clk) !rst_n |-> gray_ptr === '0)
  else $error("[GRAY] Pointer not zero during reset");

// Functional coverage: pointer wraps (MSB toggles)
cover property (@(posedge clk) $rose(gray_ptr[PTR_W-1]));

`endif

endmodule

Binary-to-Gray Conversion Reference

// Standard binary-to-gray conversion
// gray[i] = bin[i] ^ bin[i+1]  (MSB: gray[N-1] = bin[N-1])
function automatic logic [PTR_W-1:0] bin2gray;
  input logic [PTR_W-1:0] bin;
  begin
    bin2gray = bin ^ (bin >> 1);
  end
endfunction

// Verify in an assertion checker:
always @(posedge wr_clk) begin
  if (wr_en && !full) begin
    assert(wr_ptr_gray == bin2gray(wr_ptr_bin))
      else $fatal(1, "Gray/binary mismatch on write pointer");
  end
end

7. CDC Waivers and Review Process

No real SoC passes CDC analysis with zero violations — the tools are conservative and flag many legitimate crossings as potential issues. The waiver process documents every flagged crossing with a human-reviewed justification for why the violation is either safe or already mitigated by a higher-level protocol.

Waiver Categories

Waiver File Format (SpyGlass)

## cdc_waivers.sgdc — SpyGlass CDC waiver file
## Format: waive -rule <RULE> -signal <HIER_PATH> -comment <TEXT>

# Waive SRFF on status register: both loads are read-only,
# no combinational reconvergence, confirmed on schematic 2026-06-10
waive -rule CDC_SRFF \
      -signal {MyChip.u_clkb_logic.status_reg[3]} \
      -comment {Read-only fanout to RD_DATA and IRQ_STATUS. No reconvergence. Reviewed by J.Smith 2026-06-10.}

# Waive multi-bit gray-code FIFO pointer: SVA p_gray_onehot_change
# verified in sim regression suite, 500 seeds, 0 failures.
waive -rule CDC_MULTIBIT \
      -signal {MyChip.u_async_fifo.wr_ptr_gray[*]} \
      -comment {Gray-coded write pointer. SVA assertion passes 500 seeds with metastability injection. Reviewed by K.Priya 2026-06-15.}

8. CDC Sign-off Checklist

CDC sign-off is a formal gate in the design flow, typically at RTL freeze and again at gate-level netlist. The sign-off checklist must be fully checked before any waiver-incomplete design advances to physical implementation.

Why Gate-Level CDC Re-run Matters

RTL CDC analysis operates on the designer's intended synchroniser topology. Synthesis may, in rare cases, restructure or optimise away a synchroniser if it does not recognise the cell as a timing exception. A gate-level CDC re-run with the synthesised netlist and the same clock constraints catches any synchronisers that were removed, re-ordered, or inadvertently replaced with a different cell that the CDC tool does not recognise. This is especially important when the synchroniser is implemented with instantiated primitives rather than inferred flip-flops, since instantiation bypasses the synthesis don't-touch attribute.

Full Example: Async FIFO CDC Verification Testbench Skeleton

This skeleton ties together metastability injection, gray code SVA binding, and the synchroniser output stability check in a single testbench module. It is not a complete simulation — it shows the structural pattern for wiring the injection and assertion infrastructure to a real async FIFO DUT.

// =============================================================
// cdc_fifo_tb.sv — Async FIFO CDC verification skeleton
// DUT: async_fifo #(.DEPTH(16), .WIDTH(32))
// =============================================================
module cdc_fifo_tb;

// --- Clocks ---------------------------------------------------
logic clk_wr = 0;  always #2.5ns clk_wr = ~clk_wr;  // 200 MHz
logic clk_rd = 0;  always #3.33ns clk_rd = ~clk_rd; // 150 MHz

// --- DUT Signals ----------------------------------------------
logic        rst_n, wr_en, rd_en, full, empty;
logic [31:0] wdata, rdata;

// --- Metastability-injected pointer signals -------------------
logic [4:0] wr_ptr_gray_raw;  // from DUT write domain
logic [4:0] wr_ptr_gray_inj;  // after injection, fed to rd-domain sync

// Instantiate DUT
async_fifo #(.DEPTH(16), .WIDTH(32)) dut (
  .clk_wr(clk_wr), .clk_rd(clk_rd), .rst_n(rst_n),
  .wr_en(wr_en),   .wdata(wdata),    .full(full),
  .rd_en(rd_en),   .rdata(rdata),    .empty(empty),
  // Expose internal gray pointer for injection
  .wr_ptr_gray_out(wr_ptr_gray_raw)
);

// Inject metastability on wr_ptr crossing to rd domain
genvar gi;
generate
  for (gi = 0; gi < 5; gi++) begin : gen_meta
    meta_inject #(.MAX_DELAY_PS(6000)) u_mi (
      .clk_src  (clk_wr),
      .data_in  (wr_ptr_gray_raw[gi]),
      .data_out (wr_ptr_gray_inj[gi])
    );
  end
endgenerate

// Bind gray-code pointer SVA to write-pointer in DUT
bind async_fifo gray_ptr_sva #(.PTR_W(5)) u_gp_sva (
  .clk    (clk_wr),
  .rst_n  (rst_n),
  .gray_ptr(wr_ptr_gray_raw)
);

// Bind synchroniser SVA to the 2-FF sync inside DUT
bind sync_2ff sync_sva u_ss (
  .clk_b  (clk_rd),
  .rst_b_n(rst_n),
  .data_d (q2)
);

// --- Test sequence -------------------------------------------
initial begin
  rst_n = 0; wr_en = 0; rd_en = 0; wdata = 0;
  #20ns; rst_n = 1;

  // Fill FIFO completely (force pointer wrap)
  repeat(16) @(posedge clk_wr) begin
    wr_en = 1; wdata = $urandom;
  end
  wr_en = 0;
  #50ns;

  // Drain FIFO
  repeat(16) @(posedge clk_rd) rd_en = ~empty;
  rd_en = 0;

  // Simultaneous push and pop stress test
  repeat(200) @(posedge clk_wr) begin
    wr_en = !full  && $urandom[0];
    wdata = $urandom;
  end

  #200ns;
  $finish;
end

endmodule

FAQ