Multiple clocks in sequence and property

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

Below examples are not legal incase of multiple clock sequences.

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

Multiple clocks in sequence

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

For assert for multi_clock_p, on posedge clk, en is true then property pA and pB is checked.

Clock resolution in multi clock assertions

Refer Clock Resolution for better understanding.

The default or inferred clock is not allowed in multi clock assertion
The multi-clock property can not be used in procedural and clocking blocks.
It is mandatory to use an explicit clock in the multi-clock assertion.

Illegal use cases

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

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