Multi-Clock Assertions

Sequences that span clock domains

A multiclocked sequence attaches an explicit clocking event to each subsequence: @(posedge clkA) a ##1 @(posedge clkB) b means "a holds at a clkA edge; then, at the first clkB edge strictly after that, b holds." The clock in force changes at the ##1 boundary. This is how you write end-to-end checks for request/acknowledge handshakes that cross from a fast domain to a slow one.

// req asserted in clkA domain must produce ack in clkB domain
property p_cross_handshake;
  @(posedge clk_a) $rose(req) |=> @(posedge clk_b) ##[0:3] ack;
endproperty
ap_cross: assert property (p_cross_handshake);

// Sequence form: clock changes mid-sequence
sequence s_ab;
  @(posedge clk_a) a ##1 @(posedge clk_b) b;   // legal: ##1 at clock change
endsequence

Clock-crossing ## semantics — the exact rules

At a clock change, only ##1 and ##0 are legal, and their meanings shift subtly: ##1 advances to the first edge of the new clock strictly after the current time; ##0 advances to the first edge of the new clock at or after the current time (so if both clocks edge simultaneously, ##0 stays at the same simulation time, ##1 waits for the next new-clock edge).

CLOCK-CROSSING ##1 — "first strictly-later edge of the NEW clock"

time (ns)  :  0    5    10   15   20   25   30   35   40
clk_a (10n):  ┌──┐      ┌──┐      ┌──┐      ┌──┐
clk_b (20n):  ┌──┐                ┌──┐                ┌──┐
a          :       1
b          :                      1

@(posedge clk_a) a              → a sampled high at clk_a edge t=10
        ##1 @(posedge clk_b) b  → next clk_b edge strictly after t=10
                                  is t=20 → b checked at t=20  ✓ MATCH

If clk_a and clk_b BOTH edge at t=20 and 'a' matched at t=20:
  ##1 @(posedge clk_b) b  → b checked at t=40 (strictly after)
  ##0 @(posedge clk_b) b  → b checked at t=20 (at or after — same time)

Because the destination edge is "the first one after," the actual wall-clock gap depends on the phase relationship between the clocks — a property crossing from 200 MHz to 100 MHz tolerates that automatically, which is exactly why you cannot fake this with a single-clock assertion and a cycle count.

Operator restrictions in multiclocked sequences

• ##[1:3] (a range) is illegal at a clock change — only plain ##1 or ##0 may sit at the boundary between differently clocked subsequences.

• intersect, throughout, within, and first_match require a single clock — they reason about overlapping cycle windows, which is undefined across two clocks.

• and / or on sequences with different clocks are not allowed at the sequence level; use property-level and / or, where each operand carries its own clock.

• ##0 at a clock change joins at a simultaneous edge if one exists — used for clocks with known phase alignment; rare in practice.

• Local variables DO flow across the clock change — capture in the clkA half, compare in the clkB half (this makes CDC data checks possible).

• disable iff applies to the whole property and is evaluated asynchronously, so one reset can guard a two-clock property.

// ILLEGAL — range delay at a clock change
// sequence s_bad; @(posedge clk_a) a ##[1:3] @(posedge clk_b) b; endsequence

// LEGAL — cross with ##1, then a range INSIDE the clk_b domain
sequence s_good;
  @(posedge clk_a) a ##1 @(posedge clk_b) 1'b1 ##[0:2] b;
endsequence

// Local variable across the crossing: CDC data integrity
property p_cdc_data;
  logic [7:0] d;
  @(posedge clk_a) (tx_valid, d = tx_data)
    |=> @(posedge clk_b) ##[0:4] (rx_valid && rx_data == d);
endproperty
ap_cdc_data: assert property (p_cdc_data);

Worked example: four-phase CDC handshake checker

A classic synchronized handshake: the source raises req (clk_a domain) and must hold it until ack; the destination raises ack (clk_b domain) only after seeing req, and drops it only after req drops. Each rule is asserted in the domain that owns the signal, plus one multiclock property ties the round trip together.

module cdc_hs_check (
  input logic clk_a, clk_b, rst_n,
  input logic req,    // clk_a domain
  input logic ack     // clk_b domain (req_sync2, ack_sync2 are the
);                    //  2-flop synchronized versions in each domain)

  // Rule 1 (clk_a domain): req holds until synchronized ack arrives
  ap_req_hold: assert property (@(posedge clk_a) disable iff (!rst_n)
    $rose(req) |-> req throughout ack_sync2 [->1]);

  // Rule 2 (clk_b domain): ack rises only in response to synchronized req
  ap_ack_cause: assert property (@(posedge clk_b) disable iff (!rst_n)
    $rose(ack) |-> $past(req_sync2));

  // Rule 3 (multiclock): a req edge eventually produces an ack edge
  ap_round_trip: assert property (
    @(posedge clk_a) disable iff (!rst_n)
    $rose(req) |=> @(posedge clk_b) ##[0:15] $rose(ack));

  // Cover the full round trip so vacuity is visible
  cp_round_trip: cover property (
    @(posedge clk_a) $rose(req) |=> @(posedge clk_b) ##[0:15] $rose(ack));
endmodule

Why the per-domain rules carry most of the weight

Rules 1 and 2 are single-clock and reference only synchronized signals — they are immune to metastability concerns and they localize failures precisely. Rule 3 is the only true multiclock property, and it is deliberately coarse (a bounded eventually). This split — precise checks inside each domain, one loose end-to-end check across — is the recommended CDC assertion architecture.

When NOT to assert across clocks

• Raw (unsynchronized) crossing signals: simulation has no metastability, so the assertion passes in sim and the silicon still fails — assert on the post-synchronizer signal instead.

• Data buses during the unstable window: multi-bit CDC data is only meaningful when the qualifier (req/valid) says so; assert data stability while the qualifier is high, not equality cycle-by-cycle.

• Gray-code pointers in async FIFOs: assert the gray property (one bit changes per clock) inside the source domain — that is the actual design intent.

• Anything an assertion would 'prove' that timing analysis owns: setup/hold and synchronizer depth are STA/CDC-tool territory, not SVA.

Interview angle

Multiclock questions filter for CDC understanding, not syntax. Be ready for: "Why is ##[1:3] illegal at a clock change?" (a range needs one clock to count in; at a boundary there is no single clock). "Would you assert directly on a signal crossing domains?" (no — sim has no metastability; assert on the synchronized version, and check stability-while-valid for data). And the design question in disguise: "How would you check a CDC handshake?" — give the per-domain rules first, then the one bounded multiclock round-trip property. Leading with the multiclock property suggests you would write checks that pass in simulation and mean nothing in silicon.

Key takeaways

• Multiclocked sequences attach an explicit @(posedge clk) to each subsequence; the clock changes at ##1/##0 boundaries.

• ##1 at a crossing means the first strictly-later edge of the NEW clock; ##0 allows a simultaneous edge.

• Ranges, intersect, throughout, within, first_match are single-clock only — restructure so ranges live inside one domain.

• Local variables flow across the crossing — this enables CDC data-integrity checks.

• Architecture: precise single-clock assertions per domain + one loose bounded multiclock round-trip check.

Common pitfalls

• ##[1:3] at a clock boundary — compile error; put the range after the new clock takes effect.

• Asserting on raw unsynchronized signals — passes in simulation, meaningless for silicon.

• Checking multi-bit CDC data equality every cycle — data is legitimately unstable between qualifier events.

• Assuming ##1 across clocks is 'one cycle' — the real-time gap depends on clock phase; it is one destination-clock edge.

• Forgetting that property-level and/or is the only way to combine differently clocked sequences.