Hi SVA experts,
I am trying to understand the working of the following code
module tb;
bit clk1 , clk2;
logic a , b ;
always #05 clk1 = !clk1;
always #15 clk2 = !clk2;
// For 'seq' source clock is 'clk2' whereas destination clock is 'clk1'
sequence seq;
@(posedge clk2) b;
endsequence
ap1:assert property( @(posedge clk1) a |=> seq.matched ) $display("T:%0t ap1 Pass",$time);
else $display("T:%0t ap1 Fails",$time);
initial begin
#04 a = 1;
#24; b = 1;
#30 $finish();
end
endmodule
As per LRM ::
matched provides synchronization between two clocks by storing the result of the source
sequence until the arrival of the first clock tick of the destination sequence after the match. The matched status of the sequence is set in the Observed region and persists until the Observed region following the arrival of the first clock tick of the destination sequence after the match
[A] As per my understanding same rules as that for multiple clocked properties apply
For the 1st attempt at time:5 units the consequent is evaluated at the nearest destination clock i.e clk2 at time: 15units
As ‘b’ is false at time:15 units, the 1st attempt fails and the fail action block executes at time:15 units.
For the 2nd , 3rd and 4th attempt at time:15 , 25 and 35 units respectively, shouldn’t seq match at the next nearest destination clk2 at time:45units ?
I expected pass action block to execute thrice at time: 45 units
[B] If I change code to always #16 clk2 = !clk2;
Shouldn’t ‘seq.matched’ return false (1’b0) at time:16 units ?
I expected the fail action block to execute at time:16 units however I observe that it executes at time:15 units instead
[C] Would the pass / action block use the leading clock ‘clk1’ or ‘clk2’ ?
[D] If I were to add a second concurrent assertion
// @(posedge clk2) added in consequent
ap2:assert property( @(posedge clk1) a |=> @(posedge clk2) seq.matched ) $display("T:%0t ap2 Pass",$time);
else $display("T:%0t ap2 Fails",$time);
I observe different results with ‘ap2’ for both cases ([A] and [B]).
How does ‘ap2’ differ from ‘ap1’ ?