In reply to MICRO_91:
1800 is clear on multi_clocks2 and multi_clocks4.
1800 pg 446
Example 2: @(posedge clk0) sig0 ##0 @(posedge clk1) sig1
A match of this sequence starts with a match of sig0 at posedge clk0. Then ##0 moves the time to the nearest possibly overlapping posedge clk1, and the match of the sequence ends at that point with a match of sig1: if posedge clk0 and posedge clk1 happen simultaneously then the time does not move at ##0, otherwise, it behaves as ##1.
If clk0 and clk1 are not identical, then the clocking event for the sequence changes after ##0. If clk0 and clk1 are identical, then the clocking event does not change after ##0, and the preceding sequence is equivalent to the following singly clocked sequence: @(posedge clk0) sig0 ##0 sig1 which is equivalent to the following: @(posedge clk0) sig0 && sig1
1800 pg 448
For example, if s0 and s1 are sequences with no clocking events, then
@(posedge clk0) s0 |-> @(posedge clk1) s1
means the following: at each match of s0 the nearest posedge clk1 is awaited. If it happens immediately then s1 is checked without delay, otherwise its check starts at the next posedge clk1 as in case with |=>. In both cases the evaluation of s1 is controlled by posedge clk1.
On property multi_clocks1 ;
@(posedge clk0) A |=> ##0 @(posedge clk1) B;
endproperty
property multi_clocks3 ;
@(posedge clk0) A |-> ##0 @(posedge clk1) B;
endproperty
There is a discrepancy among tool vendors as to how this is processed.
I strongly believe that
A |=> ##0 @(posedge clk1) B; // should be interpreted as
A |=> 1 ##0 @(posedge clk1) B;
In my model, which I’ll share a bit later,
B==1, A==1 at t5, clk0 goes to 1 at t6 and at t13
clk1 goes to 1 at t8 and at t13.
At 13, the next posedge clk0, it processes the “1” (because of the |=> 1).
Since posedge also occurred at t13, the ##0 @(posedge clk1) B causes the evaluation of B at t13.
Another tool behaves as if it interpreted
A |=> ##0 @(posedge clk1) B; as
A |=> @(posedge clk1) B; // thus evaluated B at t8, the next posedge clk1 after posedge of clk0.
I am currently in discussion with a colleague on this. Obviously, one (or more) of the vendors
has it wrong. Stay tuned …
Ben