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

Fig. 21.6 Automaton for
complement of property
always a[+] ##1 b |=> c

a b ¬ c

s 1 s 2 s 3 s 4

true a

Solution: See Fig. 21.6 .

Discussion: This automaton contains only 4 states. Compare it with the automaton
for the complement of the property a[ * 3] ##1 b |=> c (Exercise 21.2 ). t

Efficiency Tip. The general trend is as follows: The more complex the automaton
for a property, the less efficient it is in FV.
How can a safety property be recognized? In the case the property does not
contain negations, the property is safety if it uses the following operators only:

￿ weak sequence
￿ suffix implications
￿ nexttime
￿ always
￿ until , until_with
￿ Boolean connectives and and or .
If the above operators are in the scope of a negation (or of an odd number of
negations) the resulting property is usually not safety. However, operators such as
strong sequences, s_eventually , s_until , and s_until_with become safety
properties when negated .

Example 21.22. Property nexttime (a until_with b) is a safety property
because it consists of the operators nexttime and until_with that are not in
the scope of any negation.
Property not strong (a[ * ] ##1 b) is a safety property since the strong
sequence is negated.
Property strong (a[ * ] ##1 b) implies weak (c ##[+] d) is a safety pro-
perty because it contains a strong sequence under negation in the antecedent, and
a weak sequence without negation in the consequent. Recall that A implies B is
equivalent to not A or B .
Property not ( not weak (a[ * ] ##1 b) or not weak (c ##[+] d)) is
a safety property because both weak sequences are in the scope of two negations.
t

Note that most FV tools recognize safety and liveness properties syntacti-
cally. For example, even though a until b is by definition the same thing
as (a s_until b) or always a , it is likely that most FV tools report the former
property as safety, while the latter as liveness (see [ 33 , 46 ]).