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

simulation model. If the assertion appears to be correct, the problem may lie in the
design. Further probing using simulation should then lead to the identification of the
source of the problem.

Unknown: The verification result is inconclusive. This can happen because of
timeout, memory overflow, or because of an incomplete verification algorithm. To
obtain conclusive results, it becomes necessary to refine the verification model:
to use a more aggressive or a smarter abstraction, reduce the model size, or add
auxiliary assertions. These auxiliary assertions are called lemmas : they may be
easier to prove, and when proved, they can be used as assumptions to prove the
original assertion. Another possibility is to tune the FV tool options—to choose a
specific FV algorithm, adjust its parameters, etc.
Note that it is also important to verify the completeness of the specification, that
is, whether the assertions fully represent the desired behavior and assumptions. We
leave this rather sophisticated problem out of the scope of this topic. The interested
reader may consult for example [ 32 ].

20.4.2 Lightweight Verification

Figure 20.4 represents a block diagram of the lightweight FV flow for verifying
local assertions inserted in the RTL code. Unlike in the exhaustive verification flow
where the goal is to prove formally the correctness of the model, here the objective
is to obtain a greater confidence in the overall model correctness and to detect bugs
in the design. The lightweight verification flow is much less effort-consuming than
the exhaustive verification flow.
The main purpose of this flow is bug hunting, hence only assertion failures are
investigated. Failure investigation in this case is much simpler than in exhaustive
verification; spurious counterexamples (CEX) are due only to missing assumptions.
There is no need for model refinement or tool tuning.
Lightweight verification is usually faster than the exhaustive flow because only
small parts of the RTL design affect the behavior of the local assertions.

20.4.3 Early RTL Verification

Another application of FV is early RTL verification [ 66 ]. The flow is essentially the
same as in lightweight verification, but it runs in the early stages of the design using
fast verification algorithms, such as bounded FV with small verification bounds.
The goal of this flow is to clean up obvious bugs quickly, before the simulation
environment is ready. It is well known that building a simulation environment is
a complex task, and using FV in the early stages of the design allows starting
verification earlier, thus reducing the time to market.