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

Create
specification

RTL

Specification

Check
specification in
simulation

Fix specification
or RTL

no

OK

yes

real CEX

Run
FV

Tune
verification
model or FV
options

failed unknown

Check
CEX

Check
results

passed

spurious CEX

Done

Refine
verification
model

Legend: CEX — Counterexample.

Fig. 20.3 Exhaustive formal verification flow

Success: The assertion is true for any input sequences for which all the assumptions
hold. In this case, it is tempting to say that the model is correct, but the assertion
may pass because of overconstraining assumptions or because the assertion itself is
too weak (e.g., vacuous).

Failure: A counterexample (CEX) is generated consisting of an explicit or implicit
input sequence for which all assumptions hold, but on which the assertion fails.
There may be several reasons for assertion failure. For example, the assertion may
be wrong. If the assertion is correct, the model may be underconstrained, e.g., the
applied abstraction may be too coarse. If it is not clear whether the counterexample
is real or spurious, the assertion failure should be reproduced in simulation. This
may be challenging since it requires propagating the counterexample from the inputs
of the FV model to the inputs of the simulation model. Usually, this task is done
manually or with the support of debugging tools. A fully automatic solution for
the problem of counterexample propagation is as hard as formal verification of the