Using Multi-clocked intersect operator

SystemVerilog
,
14

In reply to ben@SystemVerilog.us:

Hi Ben ,
I tried multi-clocked property for ‘within’ operator ( both LHS and RHS of ‘within’ can be a sequence expression ) :


 property  mclocks_within ;
   @(posedge clk1) ( B ##1 C ) within  @(posedge clk2) ( D ##1 E[->1] );
 endproperty
 assert property ( @(posedge clk0) A |=> mclocks_within );   //  Leading  clock ' clk0 '

I observe a compilation error with above code.

Please correct me if following reasoning is wrong :

Generally for : seq1 within seq2

Starting point of seq1 must be no earlier than starting point of seq2 , so with non-identical clocks since there is no guarantee that this occurs .
Hence ‘within’ operator is illegal for a multi-clocked property