Multi-Clock Domain Assertions: Clock Resolution

1. The Challenge of Multi-Clock Verification

When a signal generated by clk_A is sampled by logic running on an asynchronous clk_B, we can't use a simple single-clock assertion. The assertion's clock must "jump" from clk_A to clk_B to follow the data flow.

SVA provides specific mechanisms for this, but they must be used with a precise understanding of their timing semantics. A seemingly correct property can pass in simulation while hiding a real CDC bug, simply because the assertion's sampling is misaligned with the design's actual behavior.

2. Core SVA Constructs for Multi-Clock Properties

To build multi-clock assertions, we need to understand how SVA handles clock changes. The key lies in the interaction between an antecedent on one clock and a consequent on another.

Based on that reading, here are the fundamental takeaways:

• Clock Transition: You switch clock domains by explicitly specifying a new clocking event, like ... ##1 @(posedge clk_B) ....
• Concatenation Operators: To connect sequences on different clocks, you can only use ##1 or ##0.
  • s1 ##1 @(posedge clk_B) s2: The start of s2 is evaluated at the first strictly subsequent rising edge of clk_B after s1 completes.
  • s1 ##0 @(posedge clk_B) s2: The start of s2 is evaluated at the nearest, possibly overlapping rising edge of clk_B after s1 completes.
• Implication Operators: The implication operators provide the synchronization glue.
  • antecedent |=> @(posedge clk_B) consequent: The consequent starts on the next tick of clk_B (like ##1).
  • antecedent |-> @(posedge clk_B) consequent: The consequent starts on the same tick of clk_B if the clocks align, or the next tick if they don't (like ##0).

The distinction between |-> (overlapping) and |=> (non-overlapping) is subtle but critical when dealing with clocks that might have coincidental edges.

3. Essential Rules for Writing Valid Multi-Clock Assertions

The LRM (Language Reference Manual) and best practices impose strict rules on multi-clock properties. Violating them leads to compile errors or, worse, unsound verification.

Here's a summary of those critical rules:

1. Unique Leading Clock: Every concurrent assertion must have one, and only one, top-level clocking event. This event is the anchor for starting all evaluation threads.

   // ILLEGAL: Two leading clocks
   assert property ( (@(posedge clk_A) a) and (@(posedge clk_B) b) );
   
   // LEGAL: One leading clock, with clock changes inside
   assert property ( @(posedge clk_A) a |-> @(posedge clk_B) b );
   

2. No and/or Across Clocks: You cannot use operators like and, or, or intersect to combine sequences that have different clocking events.

   // ILLEGAL
   (@(posedge clk_A) a) and (@(posedge clk_B) b)
   

3. Clock Scoping is "Trapped": A clock defined inside a named sequence or a parenthesized expression does not "flow out" to subsequent parts of the larger property. The external clock flows in, but the internal clock stays in. This prevents ambiguity.

   sequence s1;
     @(posedge clk_B) b ##1 c;
   endsequence
   
   // ILLEGAL: The clock from 's1' does not flow out to 'd'. 'd' has no clock.
   assert property (s1 ##1 d); 
   
   // LEGAL: The top-level clock flows to 'd'.
   assert property (@(posedge clk_A) a ##1 (@(posedge clk_B) b) ##1 d); 
   // Here, a and d are sampled on clk_A. b is on clk_B.
   

4. A Robust Pattern for CDC Data Verification

Now let's apply this theory to a real-world problem: verifying a simple data signal crossing from clk_A to clk_B through a two-flop synchronizer.

There is a very common pitfall here related to the difference between event-driven RTL simulation and the cycle-based sampling of SVA.

Let's break down the journey from a flawed property to a robust one.

The Flawed Approach

A common first attempt might look something like this:

// FLAWED APPROACH - DO NOT USE
property cdc_check_flawed;
  logic temp_data;
  @(posedge clk_A) 
    ($changed(data_in), temp_data = data_in) |=> // Antecedent on clk_A
    ($stable(data_in)) ##1                       // Still on clk_A!
    @(posedge clk_B)                             // Finally switch to clk_B



    ##[1:4] (sync_data_out === temp_data);
endproperty

The Problem: As the paper explains (Figure 9), the property gets "stuck" in the source clock domain (clk_A) waiting for its antecedent sequence to complete. By the time the assertion's context switches to clk_B, the actual event on the data signal may have already been sampled and propagated in the destination domain. The assertion is looking for the event too late and may fail spuriously or miss bugs.

The Robust Pattern

The solution is to switch the clock context immediately after capturing the source event.

// ROBUST RTL/GLS-FRIENDLY APPROACH
property cdc_data_integrity_check;
  logic temp_data;
  @(posedge clk_A)
    ($changed(data_in), temp_data = data_in) |-> // 1. Capture event on clk_A
  @(posedge clk_B)                               // 2. IMMEDIATELY switch to clk_B



    ##[0:1]                                      // 3. Add 0-1 cycle delay for GLS robustness
    (synchronized_data_out === temp_data);       // 4. Check the result on clk_B after some latency
endproperty

Let's dissect this superior pattern:

1. @(posedge clk_A) ($changed(data_in), temp_data = data_in): The antecedent detects a change on data_in on a clk_A edge and saves its new value into a local variable temp_data. This is the trigger.
2. |-> @(posedge clk_B): This is the crucial step. We use the overlapping implication |-> to immediately change the property's clocking context to clk_B in the very same evaluation that the antecedent passed.
3. ##[0:1]: This is the subtle but vital addition from Section 4.4 of the paper. Gate-level simulations (GLS) have clock-to-q delays. This small, variable delay makes the assertion robust enough to handle the timing differences between RTL and GLS, preventing false failures in GLS. For an experienced FV role, explaining this detail shows deep practical knowledge.
4. ##[latency] (synchronized_data_out === temp_data): After some number of clk_B cycles (the synchronizer latency), we assert that the output data matches the value we saved in temp_data.

This pattern ensures the assertion "follows the data" across the clock domain boundary correctly.

Conclusion

Verifying CDC logic is a high-stakes activity, and doing it correctly with SVA requires discipline. Today you learned the formal rules and, more importantly, a practical, robust pattern that avoids common timing pitfalls.

Key Takeaways:

• Unique Leading Clock: Every assertion needs a single, unambiguous starting clock.
• Clock Transition Syntax: Use @(posedge clk) within a property to switch contexts, and use only ##0 or ##1 to connect sequences across clock boundaries.
• The Pitfall of Delayed Switching: Do not add logic on the source clock domain in the consequent of an implication. This can cause your assertion to miss the event in the destination domain.
• The Robust CDC Pattern:
  1. Detect change and store value on clk_A.
  2. Immediately switch to clk_B using |-> @(posedge clk_B).
  3. Add ##[0:1] for RTL vs. GLS robustness.
  4. After the known latency, check for the stored value at the output.

In our next lesson, we will make our assertions even more powerful and reusable by learning how to write parameterized SVA properties. This will allow us to create scalable and generic checkers for things like arbiters, FIFOs, and the CDC logic we discussed today.

🧠 Interview & Practice Drill

Time to test your understanding of these multi-clock semantics.

🎤 Interview Drill Section

1. Rapid Fire Theory:

   • What is the semantic difference between using ##0 and ##1 to connect sequences on different clocks?
   • An engineer writes assert property ((@(posedge clk_a) req) and (@(posedge clk_b) ack));. Why will this fail to compile? How would you express the intent "if req happens on clk_a, then ack should eventually happen on clk_b"?
   • You are reviewing a colleague's CDC assertion. You see they check a condition on the source clock after the implication operator, before switching to the destination clock. What risk does this introduce?
   • Why is adding ##[0:1] to a CDC assertion a good practice for ensuring robustness between RTL and gate-level simulations?

2. Resume Deep Dive Question:

   • "On your Read Return Unit FPV project, data was likely returned from a memory subsystem (on mem_clk) to a processing core (on core_clk). Describe the SVA property you would write to verify that the data payload that left the memory controller on mem_clk is the same data that arrived at the core's input buffer on core_clk a few cycles later. Walk me through the antecedent, the clock switch, and the consequent."

3. Whiteboard Problem:

   • A design has a send signal on clk_A and a recv signal on clk_B. The protocol is that for every rising edge of send, there must be a rising edge of recv within 5 cycles of clk_B. Write a robust SVA property to verify this.

🧩 Coding Exercises

1. CDC Data Bus Integrity: A 32-bit data bus data_a crosses from clk_a to clk_b, becoming data_b. The synchronizer and path have a fixed latency of 3 clk_b cycles. Write a property named a_data_bus_integrity that verifies that whenever data_a changes, data_b reflects that same value 3 clk_b cycles later. Use the robust pattern discussed in the lesson (including a local variable).

2. Request-Acknowledge Protocol: A request req_a is asserted on clk_a. This should cause an acknowledge signal ack_b to be asserted on clk_b. The clocks are asynchronous. There is no specific latency requirement, but ack_b should not be asserted before the property sees the req_a. Write a property a_req_ack_timing that asserts: if req_a rises, then at the nearest possibly overlapping edge of clk_b, ack_b must be low. (Hint: This is a perfect use case for the ##0 synchronization semantic).

3. Debug the Broken Property: An engineer tried to write a property to check that if event_a on clk_a goes high, then event_b on clk_b and event_c on clk_c must both go high eventually. Their code is below. It has at least two fundamental errors. Identify them and rewrite the property correctly.

   // BROKEN CODE
   property a_multi_event_check;
     (@(posedge clk_a) $rose(event_a)) |-> 
       ((@(posedge clk_b) s_eventually event_b) and (@(posedge clk_c) s_eventually event_c));
   endproperty