SVA with multiple clocks

/* 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 */
This is why the sequence declaration sequence multiclocks_err fails to compile.
However, if the leading clock is unique, a property can change clocks on all ops.

Test I conducted: The following code compiled and simmed OK by all.
However if I include try2:assert property ( @(posedge clk1) x |=> multiclocks_err );
then all 3 vendors flagged the sequence as an error.

module test(); 
  bit clk1, clk2, clk3, x, y, z;
  property  multiclocks ;
    @(posedge clk2) y and @(posedge clk3) z ;
  endproperty
  try1:assert property ( @(posedge clk1)  x  |=>  multiclocks );
  //The above code executes whereas on changing it to :

 /* sequence  multiclocks_err ;
    @(posedge clk2) y and @(posedge clk3) z ;
  endsequence
    try2:assert property ( @(posedge clk1)  x  |=>  multiclocks_err ); */
    initial #100;
endmodule

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or https://rb.gy/ibks5p

Getting started with verification with SystemVerilog