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

Fig. 21.4 Automaton for
complement of property
always a |=> b

a ¬ b

s 1 s 2 s 3

true

discuss here only a simple special case to give an idea of how an FV tool works
for safety properties. Some basic understanding will give insight into assertion
efficiency.
The basic idea of model checking of safety properties is simple. All states of the
FV model are partitioned into good and bad. Entering a bad state signifies a failure
of the property. Model checking of a safety property can thus be formulated as a
reachability problem: is there a path from one of the initial states of the FV model
to one of its bad states? If such a path exists, the property fails, if not, it holds. This
path, if it exists, represents a bad prefix of the property, or, informally speaking, its
finite counterexample.
Property always a provides the simplest example. All states of the FV model
containing a are good, while those not satisfying a are bad. The good states are those
in the set f v 2 V j a 2 v g , while the bad states are those in the set f v 2 V j a 62 v g .
An arbitrary safety property may be reduced to a property of this form. The
common algorithm is to build a finite nondeterministic automaton

(Sect. 21.1.4 )
corresponding to the complement of the safety property. The language of this
automaton consists of bad prefixes of the safety properties, or, in other words, this
automaton recognizes bad prefixes of the safety property 8 . The accepting states
of

A

are called the bad states . It can be shown [ 63 ] that it is always possible to
construct

A

may be synthesized into
RTL [ 14 ] such that each automaton state becomes a new RTL variable. This results
in an augmented FV model M 0 containing both variables of the original model M
and the variables corresponding to the states of

A with a single bad state. The automaton A

. If the bad state is represented by
variable b then the original safety property is equivalent to the property always b
of the augmented model.
The exact description of building the automaton of the complement of a safety
property is beyond the scope of this topic. Instead, we illustrate the idea on the
following examples.

A

Example 21.18. Build an automaton for the complement of the property always

a |=> b .
Solution: The automaton for the complement is shown in Fig. 21.4 .

Discussion: The automaton in this example is nondeterministic. It remains in the
initial state s 1 until it follows one of the evaluation attempts of a |=> b . The attempt

8 It is not required that the language L. A / of this automaton coincide with all bad prefixes of the
safety property, it is sufficient if L. A / contains some of its bad prefixes [ 46 ].