Multiple clocks in sequence and property

A multiple-clock assertion checks behavior that moves between clock domains or combines rules that run on different clocks.

Why Multiple Clocks Are Used

A design may receive a request on clkA and produce a response on clkB. A single-clock assertion cannot describe that handoff clearly. SVA allows explicit clocking events inside a sequence or inside the properties being combined.

The clock must be written next to the expression it samples. This makes it clear which clock controls each part of the check.

Multiple clocks in sequence

For writing sequence or expression for multiple clocks supported design, ##1 (single delay) is used as a concatenation operator.

@(posedge clkA) <exp_A/seqA> ##1 @(posedge clkB) <exp_B/seq_B>

The above sequence is said to be matched if

The match happens for <exp_A> starts with posedge of clkA
##1 denotes a time for the nearest subsequent posedge of clkB, and <exp_B> is evaluated for posedge clkB.

Note:

No other operator other than ##1 is used.
Since ##1 is used as a concatenate operator, so it is ambiguous to use any other delay.
Intersect, and, or operators are illegal to use.

Illegal use cases

Only ##1 can join sequence parts that use different clocks. A larger delay cannot define an unambiguous clock-domain handoff. Sequence operators such as and, or, and intersect also cannot directly combine differently clocked sequence operands.

Below examples are not legal incase of multiple clock sequences.

@(posedge clkA) seqA ##3 @(posedge clkB) seq_B
@(posedge clkA) seqA and @(posedge clkB) seq_B

Multiple clocks in Property

A property can combine other properties that have their own clocks. Property operators such as and, or, and not are legal in this form because each named property defines its sampling clock.

The and, or, not operators can be used in properties having multiple clocks

property pA;
  @(posedge clkA)  req1 | req2;
endproperty

property pB;
  @(posedge clkB)  req3 & req2;
endproperty

property multi_clock_p;
  @(posedge clk) en |=> pA and pB;
endproperty

multi_clock_p starts on clk. When en is true, the non-overlapped implication activates the consequent. Property pA then performs its check on clkA, while pB performs its check on clkB. The and operator requires both properties to succeed.

Clock resolution in multi clock assertions

Refer Clock Resolution for better understanding.

Write every clock explicitly; a default or inferred clock is not sufficient for a multiple-clock assertion.
Do not place a multiple-clock property inside a procedural initial or always block.
Do not rely on a clocking block to supply the clock for a multiple-clock property.

The following procedural uses are illegal:

Illegal use cases

//1
initial @(posedge clk) assert property (multi_clk_p);

//2
always @(posedge clk) assert property (multi_clk_p);

Declare the required clocking events inside the sequence or property, and use the property as a concurrent assertion.

assert property (multi_clock_p);

Point to remember

Use a multiple-clock sequence when one ordered event must hand off to another clock domain. Use a multiple-clock property when separate clocked rules must be combined into one pass-or-fail check.