One property, two clocks

A multiclocked sequence attaches a clocking event to each subsequence. The clock in force changes at the crossing delay, which is how one property ties a req edge in a fast domain to an ack in a slow one.

1
2
3
4

// snippet
sequence s_cross;
  @(posedge clk_a) req ##1 @(posedge clk_b) ack;
endsequence

Only ##1 and ##0 may sit at the boundary between differently clocked subsequences. Their meanings shift: ##1 advances to the first edge of the new clock strictly after now, while ##0 advances to the first edge at or after now.

The crossing, drawn

Watch req against clk_b. The attempt that starts in the fast domain lands in the slow one a moment later. The ack_sync2 row is ack after the two-flop synchronizer in the fast domain.

• Slot 0: req and ack are low. Both domains are idle.

• Slot 1: req rises in the fast domain. The round-trip attempt starts here.

• Slot 2: clk_b rises and samples req high. The crossing lands on the first slow edge.

• Slots 3 to 5: req still holds while the slow domain works. ack is low.

• Slot 6: ack rises, launched by the next rising edge of clk_b. The bounded wait is satisfied.

• Slot 7: ack_sync2 rises after two clk_a flops.

• Slot 8: the clk_a edge samples ack_sync2 high, which ends the req hold window.

• Slot 9: req drops after the synchronized ack. The handshake closes.

Because the destination edge is the first one after, the wall-clock gap depends on the phase between the clocks. A crossing from 200 MHz to 100 MHz tolerates that automatically.

Operators that need one clock

Most sequence operators reason about overlapping cycle windows, which have no meaning across two clocks. Cross with plain ##1 first, then use the operator inside the new domain.

1
2
3
4

// snippet
sequence s_good;
  @(posedge clk_a) req ##1 @(posedge clk_b) 1'b1 ##[0:2] ack;
endsequence

A CDC handshake, end to end

Each rule below is asserted in the domain that owns the signal, plus one multiclock property ties the round trip together. Precise checks inside each domain plus one loose end-to-end check across is the recommended CDC architecture.

The full handshake listing is not run in this course's checks: Verilator 5.048 does not parse multiclock properties, and Icarus 13 has no SVA sequences.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31

// not-run: Verilator 5.048 does not parse multiclock properties; Icarus 13 has no SVA sequences
module cdc_hs_check (
  input logic clk_a, clk_b, rst_n,
  input logic req,    // clk_a domain
  input logic ack     // clk_b domain
);
  logic req_s1, req_sync2, ack_s1, ack_sync2;
  always_ff @(posedge clk_b or negedge rst_n)
    if (!rst_n) {req_s1, req_sync2} <= '0;
    else {req_s1, req_sync2} <= {req, req_s1};
  always_ff @(posedge clk_a or negedge rst_n)
    if (!rst_n) {ack_s1, ack_sync2} <= '0;
    else {ack_s1, ack_sync2} <= {ack, ack_s1};

  // Rule 1 (clk_a): req holds until the 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): ack rises only while the synchronized req is high.
  ap_ack_cause: assert property (@(posedge clk_b) disable iff (!rst_n)
    $rose(ack) |-> req_sync2);

  // Rule 3 (multiclock): a req edge eventually produces an ack edge.
  // The crossing uses |=> (one ##1 step); the range sits inside clk_b.
  ap_round_trip: assert property (
    @(posedge clk_a) disable iff (!rst_n)
    $rose(req) |=> @(posedge clk_b) ##[1:15] $rose(ack));

  cp_round_trip: cover property (
    @(posedge clk_a) $rose(req) |=> @(posedge clk_b) ##[1:15] $rose(ack));
endmodule

Testbench

The DUT below keeps one clock and models both single-clock halves: two driven synchronizers plus a responder. Both properties are single-clock, so they run here; the true multiclock rule above does not. After two clean handshakes, a planted responder ignores one request.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45

module hs_half (
  input  logic clk,
  input  logic rst_n,
  input  logic bug,          // planted: the responder never answers
  input  logic req,
  output logic ack,
  output logic req_sync2,
  output logic ack_sync2
);
  logic req_s1, ack_s1;
  logic [2:0] cnt;
  logic busy;
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      req_s1 <= 1'b0; req_sync2 <= 1'b0;
      ack_s1 <= 1'b0; ack_sync2 <= 1'b0;
      ack <= 1'b0; busy <= 1'b0; cnt <= '0;
    end else begin
      req_s1 <= req; req_sync2 <= req_s1;
      ack_s1 <= ack; ack_sync2 <= ack_s1;
      if (req_sync2 && !busy && !bug) begin busy <= 1'b1; cnt <= 3'd1; end
      if (busy) begin
        if (cnt != 0) cnt <= cnt - 1'b1;
        else ack <= 1'b1;
      end
      if (ack && !req_sync2) begin ack <= 1'b0; busy <= 1'b0; end
    end
  end
endmodule

module hs_half_checks (
  input logic clk, rst_n, req, ack, req_sync2, ack_sync2
);
  int n_fail = 0;
  function automatic void fail(string msg);
    n_fail++;
    $display("[%0t] hs_half_checks: %s", $time, msg);
  endfunction
  ap_req_ack: assert property (@(posedge clk) disable iff (!rst_n)
    $rose(req) |-> ##[1:8] ack_sync2)
    else fail("req never produced a synchronized ack");
  ap_ack_cause: assert property (@(posedge clk) disable iff (!rst_n)
    $rose(ack) |-> req_sync2)
    else fail("ack rose without a synchronized req");
endmodule

2 legal handshakes: 0 reports
[385000] hs_half_checks: req never produced a synchronized ack
a request the responder ignores: 1 report
PASS: 2 handshakes passed silently, and the ignored request was reported once
[455000] hs_half_checks: ack rose without a synchronized req

Related topics

• Sampled value functions