SVA with multiple clocks

In reply to ben@SystemVerilog.us:

I am still not clear on my original doubt. In your earlier reply you commented :

However, if the leading clock is unique, a property can change clocks on all ops.

Could you please elaborate on this ? Why is it applicable for only property and not for a sequence ?

1800: 16.13.1: Differently clocked or multiclocked sequence operands cannot be combined with any sequence operators other than ##1 and ##0.
For example, if clk1 and clk2 are not identical, then the following are illegal:
@(posedge clk1) s1 ##2 @(posedge clk2) s2
@(posedge clk1) s1 intersect @(posedge clk2) s2

The above applies to both property as well as sequences , right ?

So why is it that the following is legal


  property  multiclocks ;
    @(posedge clk2) y and @(posedge clk3) z ;   // Legal
  endproperty
  try1:assert property ( @(posedge clk1)  x  |=>  multiclocks );

whereas the following is illegal


  sequence  multiclocks ;
    @(posedge clk2) y and @(posedge clk3) z ;   // Illegal
  endsequence
  try2:assert property ( @(posedge clk1)  x  |=>  multiclocks );