Hi All,
I an trying to understand the following procedural concurrent assertion
initial begin
assert property(@(posedge clk) always(a ##1 b[->1]) );
end
Let’ say the posedge of clock occurs at t1,t2,t3,t4,….
(1) If a is sampled false at t1 then assertion fails
(2) If a is sampled true at t1 then it waits for assertion of b at the nearest posedge of clock
(Q1) For (2) would a be sampled again at t2 ?
(Q2) For (2) if b is sampled true at t10 then should a be true at the next clock t11 ?
(Q3) Does the concurrent assertion essentially check for ::
(a ##1 b[→1]) ##1 ( a ##1 b[→1] ) ##1 ( a ##1 b[→1] )
i.e (a ##1 b[→1])[*infinite times]
Thanks