Are the following three assertions the same?
@(posedge clk) a |=> ##1 b[=2] ##1 c
@(posedge clk) a |=> ##[1:$] b[=2] ##1 c
@(posedge clk) a |-> ##[1:$] b[=2] ##1 c
No they are not. Next question.
Thanks, Dave.
As I understand “@(posedge clk) a |=> ##1 b[=2] ##1 c” means that after posedge clk if ‘a’ is true that ‘b’ needs to be true twice anytime after ‘a’ (first ‘b’ not necessarily after exactly one clock) and that ‘c’ needs to be true anytime after last ‘b’ (not necessarily exactly after 1 clock after last ‘b’).
From that point of view I thought that the following will be equivalent to “@(posedge clk) a |=> ##1 b[=2] ##1 c”.
@(posedge clk) a |=> ##[1:$] b[=2] ##1 C;
Could you please elaborate on why they are not equivalent?
Thanks for your time.
In the first assertion c must occur after b occurs exactly twice. If b occurs a third time before c, the assertion fails. In the other assertions with an infinite delay range, the sequence keeps searching for a match of any two occurrences of b followed by c.
The second and third assertions differ because the first occurrence of b in the third assertion can come one clock cycle earlier than the second assertion.
2 Likes
Got it. Thanks very much.
[A User] In which case can the second assertion also be written as :
@(posedge clk) a |=> first_match (##[1:$] b[=2]) ##1 c
[Ben] NO. The first_match does nothing.
** with (##1 b[=2] ##1 c) the following sequence will cause an assertion failure:
-
- -b - -b b – c // 3 b’s and no c after the 2nd b
** with (##[1:$] b[=2] ##1 c) the following sequence will cause an assertion pass:
-
- -b - -b b – c // 2 b’s and one c after the 2nd b in
the thread -" -b b – c"
##[1:$] seq is same as
##1 seq or ##2 seq or … ##n seq
Assume - - b occurs at t3, and 2nd b at t7 and 3rd b at t8, the thread ## 4 b[=2] ##1 c is a match.
2 Likes