Introduction to Assertion-Based Formal Verification - SVA: The Power of Assertions in SystemVerilog - page 439

There is nothing wrong with underapproximation. It is convenient because all
failures are correct and no spurious counterexamples are reported. One should,
however, keep in mind that the underapproximation is not sound: if no bugs are
reported the model is not necessarily correct. Of course, everybody understands this
when running simulation, but it is possible to get confused with FV. Therefore, FV
tools usually issue an appropriate message in case underapproximation is used, such
as “the assertion has not been violated up to bound 50 clock cycles”, rather than “the
assertion passed”.
Underapproximation happens inadvertently when we overconstrain the model by
writing stronger assumptions than intended. If we add the following assumption to
the original model in Fig. 20.1
always_busy: assume final (busy);
assertion req_when_idle will hold trivially, or vacuously , because idle is never
asserted in this case. This situation is dangerous because we may believe that
everything is checked, but essentially nothing is verified. Many FV tools report
assertion vacuity to help spot such cases. Unfortunately, overconstraining is usually
less obvious, and it cannot always be discovered by automatic tools. Therefore, it
is important to validate the assumptions, as discussed in Sect. 20.5 . As mentioned
earlier, trying to hit coverage points also helps to discover overconstraining.
Empty Model
An extreme case of model overconstraining occurs when there are contradictory
assumptions added to the original model, such as adding
always_busy: assume final (busy);
and
always_idle: assume final (idle);
to Fig. 20.1 .
It is possible to think that in this case all the assertions will fail in FV, but the
opposite is true—all of them will pass, vacuously. This is because the hypothesis of
the FV proof is that all the assumptions are satisfied, but this hypothesis does not
hold due to the contradiction in the assumptions. We have in fact created an empty
model —the entire constrained model contains no state due to the contradiction.
An empty model may occur not only when two assumptions are mutually
contradictory. There may be a larger set of contradictory assumptions in which no
two of them are mutually contradictory. For example,
m1: assume property (@( posedge clk) a |=> c);
m2: assume property (@( posedge clk) b |=> !c);
m3: assume property (@( posedge clk)a&&b);
Assumption m1 states that if a is true then c will be true in the next clock cycle.
Assumption m2 states the same thing about b and !c , while assumption m3 states