In reply to Shubhabrata:
In reply to ben@SystemVerilog.us:
Hello Sir, Understood what you described. But I want to know if I have written any wrong assertion . Because it looks okay to me.
ABove assertion looks OK, but it needs the first_match.
I got a couple more queries.
- In question - 7, you used two ways to write the code. In the 2nd one, I assume that you
missed writing b |->. Probably after this ( not (!$rose(a) && c) ) fits well.
I got another solution, I guess. Please look into that.
b|-> !$rose(a) until c;
See my paper Reflections on Users’ Experiences with SVA, Part II
There are lots of equivalencies. Try your code.
- In question - 8, You have solved it considering "… must appear … ". But the
problem says “… may appear…”. And, I think it’s correct. I tried something. Please look into this too.
!a[*1:$] |-> b[=0:1] ##1 a;
BAD style! !a[*1:$] |-> … causes unnecessary multiple threads at each attempt;
just use !a
If b “may” appear, you are essentially say that it does not matter if it does or does not appear. Thus, b is not in the equation.
Same thing in people’s behavior: “I go to the airport; it may or may not rain, I am taking the plane to go to Las Vegas”. The rain is not consequential.
Thus, you can write
!a |-> a[->1];