Every crossing carries protocol rules. Requests hold until acknowledged, and data stays stable under request.
Acknowledgements answer requests, and source Gray pointers move one bit per step. The listing below drives a legal Gray sequence in which 5 destination samples legally skip Gray steps; a mutation that makes the source Gray pointer jump two bits fires a_gray_one_bit.
Each slot is one source clock cycle (5 ns); clk is the destination clock at half the rate. src_bits and dst_bits count the bits that changed since the previous value in each domain.
Slots 0 to 7: gray_src steps 000, 001, 011, 010, 110, 111, 101, 100, and from slot 1 on src_bits is always 1. The source property holds.
Slot 3: the destination samples 011 after 000. It never saw 001, so two bits changed and dst_bits is 2.
Slots 5 and 7: every later sample also changes two bits (110, then 101). A one-bit check on dst_q would fire on every sample of a correct design.
Violation driven | Property that fired | Message |
|---|---|---|
|
| Assertion failed in …dut.a_req_holds |
Data bus changes while |
| Assertion failed in …dut.a_data_stable |
|
| Assertion failed in …dut.a_ack_needs_req |
Gray pointer changes two bits at once |
| Assertion failed in …dut.a_gray_one_bit |
Verilator supports the common SVA subset: implication, $past, $stable, $rose and fixed delays. Older Verilator releases did not support ranged delays such as ##[1:5]; Verilator 5.048 runs them with --timing --assert. Check your tool version.
Keep checks in the simple subset so they run in every assertion-capable flow (Verilator with --assert, commercial simulators, formal).
Check | SVA sketch |
|---|---|
Pulse spacing at least N cycles |
|
One-hot select |
|
FIFO never overflows |
|
Valid stays until ready |
|
Reset leaves protocol idle |
|
a_data_stable check $past(req) as well as req?To avoid flagging the very first cycle of the request, in which the data may legitimately change from the previous value. The rule only applies once the request has been high for a cycle.
The checker module plus a testbench driving a legal handshake and a legal Gray sequence. Run it with Verilator (verilator --binary --timing --assert); Icarus cannot parse concurrent assertions.
// not-run: concurrent assertions and default clocking need Verilator (verilator --binary --timing --assert); Icarus 13 cannot parse them
// Handshake signals are local to clk. The Gray pointer has its own source clock/reset.
module cdc_checks (
input logic clk, rst_n,
input logic req, ack,
input logic [7:0] data,
input logic src_clk, src_rst_n,
input logic [4:0] gray_src
);
default clocking cb @(posedge clk); endclocking
default disable iff (!rst_n);
// 1. A request stays high until it is acknowledged.
a_req_holds: assert property (req && !ack |=> req);
// 2. The data bus is stable for as long as req is high.
a_data_stable: assert property (req && $past(req) |-> $stable(data));
// 3. An acknowledge only appears in answer to a request.
a_ack_needs_req: assert property ($rose(ack) |-> $past(req));
gray_source_checks g (.src_clk, .src_rst_n, .gray_src);
endmodule
// Separate clocking scope prevents the handshake clock from sampling the source pointer.
module gray_source_checks (
input logic src_clk, src_rst_n,
input logic [4:0] gray_src
);
default clocking cb @(posedge src_clk); endclocking
default disable iff (!src_rst_n);
logic src_past_valid;
always_ff @(posedge src_clk or negedge src_rst_n)
if (!src_rst_n) src_past_valid <= 1'b0;
else src_past_valid <= 1'b1;
a_gray_one_bit: assert property (
src_past_valid |-> !$isunknown(gray_src) &&
$countones(gray_src ^ $past(gray_src)) <= 1);
endmodule
module tb_cdc_checks;
logic clk = 0, rst_n = 0, req = 0, ack = 0;
logic [7:0] data = 0;
logic src_clk = 0, src_rst_n = 0;
logic [4:0] src_bin = 0, gray_src = 0, dst_g1 = 0, dst_g2 = 0, dst_prev = 0;
int skipped_steps = 0;
cdc_checks dut (.*);
always #5 clk = ~clk;
always #1 src_clk = ~src_clk;
initial begin
repeat (2) @(negedge src_clk);
src_rst_n = 1;
end
always_ff @(posedge src_clk)
if (!src_rst_n) begin src_bin <= '0; gray_src <= '0; end
else begin
src_bin <= src_bin + 5'd1;
gray_src <= (src_bin + 5'd1) ^ ((src_bin + 5'd1) >> 1);
end
always_ff @(posedge clk)
if (!rst_n) begin dst_g1 <= '0; dst_g2 <= '0; dst_prev <= '0; end
else begin
dst_g1 <= gray_src; dst_g2 <= dst_g1; dst_prev <= dst_g2;
if ($countones(dst_g2 ^ dst_prev) > 1) skipped_steps <= skipped_steps + 1;
end
initial begin
repeat (2) @(negedge clk);
rst_n = 1;
// one legal handshake
@(negedge clk) begin req = 1; data = 8'h12; end
repeat (2) @(negedge clk);
ack = 1;
@(negedge clk) req = 0;
@(negedge clk) ack = 0;
// Source steps remain legal even when the slower destination skips values.
repeat (3) @(negedge clk);
if (skipped_steps == 0) $fatal(1, "test did not exercise skipped destination Gray values");
$display("PASS: source Gray steps satisfy the property; %0d destination samples legally skip steps", skipped_steps);
$finish;
end
endmoduleThe directed example requires observed multi-bit destination jumps while the source property remains legal. The ideal destination flops here illustrate sampling scope.
Revised listing, run with Verilator 5.048 (--binary --timing --assert, 2026-10-16): prints PASS with 5 destination samples that legally skip Gray steps. A mutation that makes the source Gray pointer jump two bits fires a_gray_one_bit.
The handshake rows in the violation table come from an earlier version of the bench and are not re-run against the revised checker. Re-run the source two-bit-jump mutation against gray_src to confirm detection. The ideal destination flops illustrate sampling scope, not physical CDC signoff.