In reply to ben@SystemVerilog.us:
Would like to add a point related to throughout operator being illegal as a multi-clocked property.
Syntax for throughout operator as per Syntax 16-11 :
expression_or_dist throughout sequence_expr
i.e LHS of throughout operator can’t be a sequence or sub-sequence . Only a signal or expression is valid as LHS.
As a result ‘throughout’ operator as a multi-clocked property is illegal.
To summarize multi-clocked properties :
1) Using and/or operator is Legal :
property mclocks_and_or ;
@(posedge clk1) B and @(posedge clk2) C ; // Could be "or" operator as well
endproperty
ap0:assert property ( @(posedge clk0) A |=> mclocks_and_or ); // Leading edge present
2) Using intersect operator is Illegal as the requirement for intersect operator is that the length of the sequences must match
( which can’t be guaranteed due to non-identical clocks ):
property mclocks_intersect ;
@(posedge clk1) B intersect @(posedge clk2) C ; // Illegal due to unequal length
endproperty
ap0:assert property ( @(posedge clk0) A |=> mclocks_intersect );
3) Using throughout operator is Illegal as the LHS of throughout operator can’t be a sequence :
property mclocks_throughout ;
@(posedge clk1) B throughout @(posedge clk2) C ; // Illegal as LHS is sequence
endproperty
ap0:assert property ( @(posedge clk0) A |=> mclocks_throughout );
Thus only and/or/not operators are valid within a multi-clocked property.
EDIT : As Ben pointed implies operator is valid as well