CDC and RDC with Formal

Structure Finds the Synchroniser; a Property Checks the Value

A structural CDC check reads the netlist: every flop in one domain whose input comes from another must pass through a recognised synchroniser. That catches a missing synchroniser. It cannot know whether the value sent through a correct one is safe to send.

That is a property. On the source clock: $countones(ptr ^ $past(ptr)) <= 1. The gray pointer gives BMC PASS to depth 20 and Prove PASS (k = 4); the binary count gives FAIL at reported step 4.

Why One Bit Is the Rule

A flop that samples a bit as it changes may settle either way. If several bits move at once, each may settle differently. On this engine a flop never goes metastable, so the lab adds a free input, meta, that chooses old or new for every moving bit (F1.6).

The binary pointer fails, FAIL at reported step 5: the reader sees 3. The gray pointer gives BMC PASS to depth 20 and Prove PASS (k = 4).

Two Real Clocks

With two clocks and plain flops, the binary pointer passes: in the model every capture is clean. Only with racing bits modelled does it fail, and the gray pointer still passes. The cover shows that run moved data across, so its pass is not empty.

The lesson for any CDC proof: the model decides what can go wrong. Commercial CDC tools add such metastability models or ask for them; check which your flow uses before trusting a pass.

Reset Domain Crossings

rst_a asserted (async to clk_b)
  -> flop in domain A changes now
  -> domain-B flop samples it mid-change

structural: which crossings see rst_a?
property:   while rst_a is asserted,
            the domain-B consumer is held

An asynchronous reset in one domain changes the crossing flop's output at a time the other domain did not choose. This engine refuses asynchronous resets, so the page draws the check and leaves the run to a full two-clock flow.

Asked in Interviews

Try It

assert property (@(posedge clk) disable iff (rst) $countones(ptr ^ $past(ptr)) <= 1);
assert property (@(posedge clk) disable iff (rst) sync1 == $past(ptr) || sync1 == $past(ptr, 2));

  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg [3:0] ptr_q2=0;   // ptr two edges ago
  reg live=0;
  always @(posedge clk) begin ptr_q2 <= ptr_q; live <= !rst; end
  always @(posedge clk) if (!rst && live) assert(sync1 == ptr_q || sync1 == ptr_q2);

[options]
mode bmc
depth 20
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv
prep -top gray4
[files]
design.sv

module cdc2(input winc, input [3:0] meta);
  (* anyconst *) reg [3:0] wstep, rstep;   // clock model: two phase accumulators
  reg [3:0] wph=0, rph=0;
  always @(*) assume(wstep != 0 && wstep <= 4'd8 && rstep >= wstep && rstep <= 4'd8);
  always @($global_clock) begin wph <= wph + wstep; rph <= rph + rstep; end
  wire wclk = wph[3], rclk = rph[3];
  reg [3:0] bin=0, ptr=0;                  // write domain
  wire [3:0] bin_next = bin + winc;
  always @(posedge wclk) begin bin <= bin_next; ptr <= bin_next; end
  reg [3:0] ptr_g=0, ptr_prev=0;           // ptr one global tick ago, and before its last change
  always @($global_clock) begin ptr_g <= ptr; if (ptr != ptr_g) ptr_prev <= ptr_g; end
  wire [3:0] moving = ptr ^ ptr_g;
  reg [3:0] sync1=0, sync2=0;              // read domain: two-flop synchroniser
  always @(posedge rclk) begin
    sync1 <= (ptr & ~moving) | (moving & ((meta & ptr) | (~meta & ptr_g)));
    sync2 <= sync1;
  end
  always @($global_clock) assert(sync1 == ptr || sync1 == ptr_g || sync1 == ptr_prev);
endmodule

[options]
mode bmc
depth 40
multiclock on
[engines]
smtbmc yices
[script]
read_verilog -formal -sv cdc2.sv
prep -top cdc2
[files]
cdc2.sv

1. Break the converter

   Run as it is: FAIL at reported step 4. Which count does the trace stop at, and why not 7 to 8?

2. Restore gray

   Put the converter back: BMC PASS to depth 20. Switch to mode prove, depth 4: Prove PASS (k = 4).

3. Race the bits

   Run gray_sync with the binary pointer: FAIL at reported step 5. Read meta at the failing step.

4. Race gray bits

   Restore the gray pointer in gray_sync: BMC PASS to depth 20.

Check Yourself

module gray4(input clk, rst, inc, output reg [3:0] ptr=0);
  reg [3:0] bin=0;
  wire [3:0] bin_next = bin + inc;
  always @(posedge clk)
    if (rst) begin bin <= 0; ptr <= 0; end
    else begin
      bin <= bin_next;
      ptr <= bin_next;   // bug: the binary count crosses
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg [3:0] ptr_q=0;   // last cycle's ptr
  always @(posedge clk) ptr_q <= ptr;
  always @(posedge clk) if (!rst) assert($countones(ptr ^ ptr_q) <= 1);
`endif
endmodule