In reply to MICRO_91:
CORRECT BEHAVIOR: in the expressions below,
seq1: @(posedge clk0) A |=> ##0 @(posedge clk1) B
// same as
seq1_equiv: @(posedge clk0) A |=> @(posedge clk0) 1 ##0 @(posedge clk1) B
Question: when are these 2 assertions equivalent?
k0n01: @(posedge clk0) A |=> ##0 @(posedge clk1) B // is equivalent to
k0n01: @(posedge clk0) A |=> @(posedge clk0) 1 ##0 @(posedge clk1) B
k0n1 : @(posedge clk0) A |=> @(posedge clk1) B
k0n01 and kn01 would behave the same if the clocking event floowing the
first @(posedge clk0) is
@(posedge clk0 ) and then @(posedge clk1) or
@(posedge clk0) simulataneously with @(posedge clk1)
The reason: |=> @(posedge clk0) 1 ##0 @(posedge clk1) B
Following the |=> we’re waiting for(posedge clk0) followed by @(posedge clk1) B
// EPWave Waveform Viewer wave as expected (correct)
// EPWave Waveform Viewer wave incorrect,
// EPWave Waveform Viewer wave incorrect
// (7) - EDA Playground code
WRONG BEHAVIOR The ##0 version delays the consequent check to the next posedge of clk1.
Ben