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

We can formulate our findings in terms of the counterexamples: every coun-
terexample of a1 has a finite prefix such that all its extensions are counterexamples.
On the contrary, in the case of a2 , every finite trace has an extension that is not a
counterexample. Informally speaking, all the counterexamples of the assertion a1
are finite, whereas all the counterexamples of the assertion a2 are infinite. In fact all
the counterexample of the assertion a2 have the form w D: a ! .
This leads us to the following property classification. Property p is safety if
each counterexample has a finite prefix, and all its extensions are counterexamples.
Such a prefix is a bad prefix . The property p is (pure) liveness if every finite trace
has an extension that is not a counterexample. Speaking informally, we can say
that safety properties check that something bad never happens, whereas liveness
properties check that something good eventually happens. Safety properties may
fail in simulation, whereas pure liveness properties cannot. Only FV can fully check
liveness properties as FV can deal with infinite traces. 7

The vast majority of all

properties used in practice are safety.
Are there properties that are neither safety nor liveness? Yes, such properties
exist. As an example, consider the property a s_until b . The trace w 1 D . : a ^
: b/b:::has a bad prefix . : a ^: b/; all the extensions are counterexamples, while
the trace w 2 D .a ^: b/ ! provides an infinite counterexample, such that each finite
prefix has an extension that is not a counterexample. Indeed, on w 1 there is no a
before the first occurrence of b , and on w 2 b never happens. Such properties are
called hybrid or general liveness properties. These properties have both a liveness
and a safety component.
For our purpose, the distinction between the pure and general liveness properties
is not that important, and we will reserve the term liveness for both pure and general
liveness properties. We explicitly use the terms “pure” or “general” when we need
to distinguish between these two types of liveness.
The notions of safety and liveness are fundamental in FV. The users of FV tools
should be able to determine for any property whether it is safety or liveness, and try
to use safety properties as much as possible. This is necessary for FV to be efficient,
as checking safety is generally more efficient than checking liveness. To help the
user write efficient properties, some FV tools report the type of each property, safety,
or liveness.

21.4.1 Safety Properties

Algorithms for formal verification of assertions are called model checking . A sys-
tematic description of model checking is beyond the scope of this topic, and we

7 Some liveness properties may pass in simulation, like property s_eventually a if a is
observed to hold at one point in time. However, there are liveness properties that can neither fail
nor pass in simulation, like the property s_eventually always a .