I’m confused how assertions are evaluated when if-else statement is used inside a property.
I tried the code below, and it looks like that when the antecedent in line number 7 is not met, the assertion is evaluated as true.
I would like to ask for a clarification.
1 property my_property;
2 @(posedge clk)
3
4 if(a) // a is low
5 sig1 & sig2 -> ##1 sig_A
6 else
7 sig1 & sig2 & sig3 -> ##1 sig_B;
8
9 // sig3 is low but this assertion is evaluated as true. This is causing a false positive result.
10 endproperty : my_property
What to do so that this assertion will not be evaluated (neither true nor false) when antecedent in line number 7 is not met, without separating the conditions into two different assertions?
What is the natural language requirement you are trying to model as an assertion? When ‘a’ is low, do you expect to see ‘sig1 & sig2 & sig3’ always, followed by ‘sig_B’? Do you only expect ‘sig1 & sig2’ to be true when ‘sig3’ is high? A detailed description of what you want to achieve would help.
In reply to Reuben:
What is the natural language requirement you are trying to model as an assertion? When ‘a’ is low, do you expect to see ‘sig1 & sig2 & sig3’ always, followed by ‘sig_B’? Do you only expect ‘sig1 & sig2’ to be true when ‘sig3’ is high? A detailed description of what you want to achieve would help.
Hi. I just want to know how if-else statement is evaluated in assertion property.
I’m analyzing someone’s code and that is how he wrote his assertion. When I ran the simulation, I saw that his assertions are passing even though the antecedents are not yet met. ‘a’ is always low, sig3 never becomes high, but the assertion is passing. How come?
The property gets attempted on each clock cycle. If a is low, the the else block is taken and the property sig1 & sig2 & sig3 → ##1 sig_B is evaluated. Since sig3 is low, the whole antecedent is false. For implication, a false antecedent is a vacuous pass. Since the property under the else evaluated to pass, the whole if/else property evaluates to pass. I couldn’t find the vacuity semantics for if/else explicitly written out int he LRM, but I presume that they are similar to those for implication. This means that, since the evaluation of the property under the else was vacuous, then the entire evaluation of the if/else is also vacuous.
Also, I noticed that you were also asking how to have the tool not mark the assertion as passed. You can only do this with a disable iff. I’m not sure what the best practices w.r.t. using this are, but you for sure want to use $sampled(…) inside it due to the way the semantics are defined. I guess in your case it would look something like:
The issue with vacuity you will have regardless of whether you split your assertion into two smaller assertions or not. Tools usually either don’t collect vacuous passes by default or if they do they categorize them separately.
I see. So this is called a “Vacuous Pass”. When there is no match in the antecedent, then evaluation of the implication succeeds vacuously and returns true.
I also found out that in order to avoid this, a cover property is used since it does not cover vacuous passes.
Thanks for the help. I finally understand this issue and why a cover property is sometimes used together with assert property.
I guess the tool I am using is covering vacuous pass. I can see in the coverage report that the number of hits is as much as 22,000, wherein I’m only expecting it to be less than 10 hits.
Actually I tried $assertvacuousoff(0) but the tool does not recognize this system task.
So maybe the only way to avoid false positive coverage hits is to split this assertion into different sequences.
These vacuous passes are sometimes pain and does not seem to serve real purpose. For instance, once I swapped clock/reset connections in formal verification setup and all properties magically passed. After seeing property coverage only we got to know that nothing actually got covered. Beware of vacuous misreadings!
This isn’t strictly true. Another example of vacuity is given in section 16.12.16 of the 2012 LRM, where a case property without a matching case item and no default passes vacuously. You can say that such a case is the same as unrolling each case item into an own implication property.
Implication is what “generates” vacuity, but it’s not just possible if you explicitly see an implication property (i.e. ‘|->’ or ‘|=>’ as described in 16.12.6), but also for other properties that have “implication” built into them.