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

20.3 Approximation

Sometimes approximation [ 18 ] is used in formal verification. While exact methods
should always return accurate results, approximation-based methods can return an
inaccurate result due to approximation error: either a false negative , in which case
failure is reported for an assertion that should pass, or a false positive , in which case
success is reported for an assertion that should fail. According to the error types
introduced by the approximation, one distinguishes between overapproximation ,
which may introduce false negatives, and underapproximation , which may intro-
duce false positives. Overapproximation is sound , meaning that a result of success
is always accurate (i.e., free of approximation error). Underapproximation is safe ,
meaning that a result of failure is always accurate.

20.3.1 Overapproximation

Overapproximation occurs either automatically as part of the verification strategy
of FV tools, in which case it is transparent to the users, or manually when a design
model is abstracted. The abstract model is usually simpler than the original one
and allows more behaviors. If the assertion is proven on this abstract model, it
also holds on the original model. If the assertion fails on the abstract model, the
counterexample may be spurious , i.e., impossible in the original model. Manual
checking of whether counterexamples are spurious may be difficult, especially
when there are many of them. Therefore, overapproximation may lead the user to
ignore assertion failures, thus missing true bugs. The benefit of model reduction that
enables a successful FV run has its cost in the analysis and elimination of spurious
counterexamples. This is discussed in more detail below.
Overapproximation may also happen inadvertently, for example, when one or
more assumptions is missing. In this case the model allows for more unintended
behaviors, hence false negatives are likely to occur. This is why a validated thorough
system specification is important.
Another common case of overapproximation happens when we try to formally
verify only a part of a bigger model by removing some subcomponents or blocks of
statements. Figure 20.1 shows a toy module generating signal req : req is asserted
only when the system state is idle . Assertion req_when_idle checks that if idle
is asserted, then in the next clock cycle req is asserted unless rst happens.
Let us assume that we wish to verify a smaller model. We manually delete the
assignment statement on Line 3 . What we obtained is an overapproximated model.
Now the assertion will fail since idle may assume any value at any time. 2

This toy

2 It is possible to argue that since idle is now unassigned it will keep the value X all the time.
This is true in simulation, but FV tools usually consider undriven variables, like idle ,asafree
variable which may assume any value at any time.