Assertion Statements - SVA: The Power of Assertions in SystemVerilog - page 89

Table 4.2 Checking assertions in simulation and in FV

Assertion Simulation Formal verification

Check whether an assertion is vio-
lated on a given simulation trace

Check whether an assertion can be
violated while respecting all speci-
fied assumptions. If yes, may report
a counterexample

assert

Check whether an assumption is vio-
lated on a given simulation trace
(same as for assertions)

Use as a constraint when check-
ing assertions and coverage points.
The assumption correctness is not
checked

assume

restrict Ignore Use as a constraint when checking

assertions and coverage points (same
as for assume )

cover Check whether a coverage condition

is met on a given simulation trace

Check whether the coverage condi-
tion can be met while respecting all
specified assumptions. If yes, may
report a coverage witness

4.7.3.2 Checking Coverage in Formal Verification

In FV, the coverage condition (called also coverage point) is checked for its
feasibility, that is, whether it can be reached when all the assumptions are met. FV
tools either report that a coverage point cannot be reached, or provide a reachability
witness, as discussed in Sect. 20.1 .

4.8 Summary of Checking Assertions

Table 4.2 summarizes checking SVA assertions in simulation, 11

and in FV.

Exercises

4.1. What do assertions check?

4.2. Write four versions of an assertion checking that all bits of some packed bit
vector are set to 1: immediate, deferred observed, deferred final, and concurrent.
Explain the difference between them.

4.3. What is the purpose of assumptions?