In reply to ben@SystemVerilog.us:
My above understanding is correct. Let’s have a reiteration:
@(posedge clk0) A |=> ##0 @(posedge clk1) B;
is similar to writing
@(posedge clk0) A |=> ##0 s; // where s is some sequence.
The ##0 is still on clk0 and is equivalent to
@(posedge clk0) A |=> 1 ##0 s;[b]
I.e.,
@(posedge clk0) A |=> 1 ##0 @(posedge clk1) B;[/b]
There is a one clock cycle of clk0 before it starts searching for a tick of clk1,
which due to ##0 can occur at the same time as the 2nd tick of clk0.
@(posedge clk0) A |=> ##0 @(posedge clk1) B; // (multi_clocks1) k0n01+=1;
@(posedge clk0) A |=> @(posedge clk1) B; // (multi_clocks2) k0n1+=1;
@(posedge clk0) A |-> ##0 @(posedge clk1) B; //(multi_clocks3) k001+=1;
@(posedge clk0) A |-> @(posedge clk1) B; //(multi_clocks2) k01+=1;
multi_clocks1 and multi_clocks2 are not equivalent
multi_clocks3 and multi_clocks4 are not equivalent
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Cohen_Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog