Formal Verification and Models - SVA: The Power of Assertions in SystemVerilog - page 460

It follows that a contradictory model will make cover properties unsatisfiable,
indicating to the user that something is not correct in the model if the expectation is
that the cover should be reachable.

Example 21.17. Property s_eventually o is satisfiable on model M from
Example 21.8 because the trace : i;::: satisfies p (in this trace the value of i
at time 0 is 0, and thus the value of o at time 1 is 1). The same property is not
valid on M because it is not satisfied on any trace of the form i ! , which are legal
traces of M . The failure of the assertion on i ! indicates that some assumption on
the behavior of the input i is needed, such that i may not stay constant 1 from some
point in time on. t

21.3.4 Constraining a Model with Assumptions

If assertion p holds on model M then it also holds on M composed with
assumption q. This is because the composition M jj q may not accept more traces
than model M alone does.
The situation with coverage is the opposite: if property p is covered on a
composition M jj q, then it is also covered on model M alone, since M accepts
all traces that M jj q does.
Informally speaking, adding assumptions increases the chances of a property to
become valid, but decreases its chances of being covered. This does not necessarily
mean that adding assumptions makes FV easier for assertions and more difficult
for coverage goals. For example, adding assumptions may make the formulas used
in FV more complicated, and thus make the work of FV tools much harder. See
Sect. 20.3 for a discussion on approximation and abstraction.

21.4 Safety and Liveness

Compare the following two assertions a1 and a2 :
a1: assert property ( always a);
a2: assert property ( s_eventually a);
Can these assertions fail in simulation? Assertion a1 certainly can if in some global
clock tick the value of a is 0. We can even say that if this assertion is violated on
some infinite trace then there is a finite prefix of this trace where this assertion is
violated, namely, the trace fragment until (including) the first occurrence of a=0 .
But what about assertion a2 ? We can simulate this assertion during millions of ticks
and never see a taking on the value 1. Does it mean that assertion a2 is violated in
simulation? Obviously not: had we simulated a2 a few more ticks we might discover
that a holds. Assertion a2 cannot fail in simulation except at the end as discussed in
Chap. 10 .