Using ##0 Clock delay with Implication Operators

SystemVerilog
,
6

In reply to ben@SystemVerilog.us:

Ben ,

multi_clocks3 and multi_clocks4 arenot equivalent

I observe that all tools agree that these two are indeed equivalent ( tested for both non-overlapping as well as overlapping clocks ) :


 property  multi_clocks3 ;
    @(posedge clk0) A |-> ##0 @(posedge clk1) B;
 endproperty
 
 property  multi_clocks4 ;
    @(posedge clk0) A |-> @(posedge clk1) B; // Without ##0 in consequent
 endproperty

The discrepancy lies with multi_clocks1 and multi_clocks2 . Some tools agree with your explanation while others treat multi_clocks1 and multi_clocks2 as equivalent

The expected output would be clearer had the LRM discussed it. Hopefully it gets resolved in future versions of the LRM.