Question

The following are examples of multiple-clock specifications:

sequence s1;
    @(posedge clk1) a ##1 b; // single clock sequence
endsequence

sequence s2;
    @(posedge clk2) c ##1 d; // single clock sequence
endsequence

1) multiple-clock sequence

sequence mult_s;
    @(posedge clk) a ##1 @(posedge clk1) s1 ##1 @(posedge clk2) s2;
endsequence

2) property with a multiple-clock sequence

property mult_p1;
    @(posedge clk) a ##1 @(posedge clk1) s1 ##1 @(posedge clk2) s2;
endproperty

3) property with a named multiple-clock sequence

property mult_p2;
    mult_s;
endproperty

4) property with multiple-clock implication

property mult_p3;
    @(posedge clk) a ##1 @(posedge clk1) s1 |=> @(posedge clk2) s2;
endproperty

5) property with named sequences at different clocks. In this case, if s1 contains a clock, then it must be identical to (posedge clk1). Similarly, if s2 contains a clock, it must be identical to (posedge clk2).

property mult_p5
    @(posedge clk1) s1 |=> @(posedge clk2) s2;
endproperty

6) property with implication, where antecedent and consequent are named multi-clocked sequences

property mult_p6;
    mult_s |=> mult_s;
endproperty

7) property using clock flow and overlapped implication:

property mult_p7;
    @(posedge clk) a ##1 b |-> c ##1 @(posedge clk1) d;
endproperty

Here, a, b, and c are clocked at posedge clk.

8) property using clock flow and if...else:

property mult_p8;
    @(posedge clk) a ##1 b |->
    if (c)
        (1 |=> @(posedge clk1) d)
    else
        e ##1 @(posedge clk2) f ;
endproperty

Here, a, b, c, and e are clocked at posedge clk.