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
[A] For the 1st , 2nd , 3rd attempt at time:5 , 15 & 25 units respectively as seq.matched would return 0 the assertions fails at time: 15,25 & 35 units respectively.
(Q1) At the overlapping edge at time: 45, ‘b’ is true so for the 4th attempt which starts at time:35, shouldn’t seq.matched return 1 ?
I expected pass action block to execute at time: 45 units
Does matched return true on the same clock (overlapping) that it matches ?
As per LRM 16.13.6 ::
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
I am trying to decode the meaning of “until the arrival of the first clock tick of the destination sequence after the match”
(Q2) Would the overlapping edge at T:45 be considered first clock after the match or would it consider the next destination clock edge at T:55 ?
Since the matched status is set in observed region at T:45 and the assertion evaluation occurs in observed region, shouldn’t seq.matched return true at T:45 (overlapping clock)
[B] (Q3) Would the pass / action block use the leading clock ‘clk1’ or ‘clk2’ ?
[C] 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]).
(Q4) How does ‘ap2’ differ from ‘ap1’ ?
