IFV PSL , using VHDL comparison operator

Adding the opposite of an assertion (one expected to "fail") is a useful sanity check. It can help uncover problems with a formal verification setup.

In this instance, having both assertions pass is a possible result. An assertion can pass "vacuously" if the prefix of the assertion can never be reached. As an example, the assertion "a |=> b" will pass if 'a' can never occur. If 'a' is impossible, both "a |=> b" and "a |=> not b" will pass because neither can ever reach the failing state.

So the first thing to look for is whether or not IFV says that the "trigger" of these assertions passes. If the trigger check fails, then the prefix of the assertion is impossible and the assertion itself will pass.

Hi,

in this case it may be that the vacuity starts in the next cycle after the trigger. So please check whether the "Trace" check fails.

Regards, Joerg.

No, it does not. You need to look a the trace to detect such kind of vacuity. Example:

 assume a |=> b;

 assume a |=> !b;

The 2 constraints create vacuity after the first occurence of "a". There is no solution for b that satisfies the constraints.

assert a |=> false

The property trigger is pass, but the trace is fail. Regardless, what the RHS says... In IEV you would get a deadend in such a situation

Joerg.

Hi Jentil,

a trace or a trigger is a reachability check, just like any other cover statement. To understand why something is unreachable, you need to de-assemble the elements of that sequence or condition and anaylze their reachability, respectively. For example, if the following sequence is unreachable, you need to check if the sub components are reachable:

cover { a; b; c } is unreachable

Check sub components:

cover {a; b } is also unreachable

cover { a } is reachable

So you look at the driver of b to determin why it is unreachable and so forth.

Joerg.