Basic Properties - SVA: The Power of Assertions in SystemVerilog - page 93

Fig. 5.1 Boolean property e

clock ticks

Boolean property e is true in clock tick i iff Boolean expression e is true in clock
tick i .

Boolean Expressions and Properties. What is confusing is how we can distinguish
between Boolean expression and Boolean property if they both have exactly the
same syntax? The answer is simple: if a Boolean is used in a context where a
property is expected, then it is a Boolean property. For instance, on the one hand,
e in the property expression nexttime always e from Example 5.1 is a Boolean
property since a property operator always expects a property as its argument. On
the other hand, in the expression ~ e , e is a Boolean expression, but not a Boolean
property, since the bitwise negation operator ~ requires a Boolean 2 expression, and

it cannot accept a property as its argument.
Our definition of Boolean property explains the meaning of the sentence “ e is true
in clock tick i ”. However, in the general definition of property given in the beginning
of this chapter we defined the property truth relative to the entire trace, and not in a
specific clock tick. So what does it mean that e is true on a whole trace, and not just
in a specific clock tick of this trace? This question is general and it may be answered
for any property, not just for a Boolean one. Consequently, we give a general answer
to this question for arbitrary property p .

Property p is true on a trace iff it is true in clock tick 0 of this trace.

This implies that Boolean property e is true iff e is true in the clock tick 0, as
shown in Fig. 5.1 .

Example 5.2. If a DUT contains three signals a , b , and c , and in clock tick 0 a=1 ,
b=1 , and c=0 then the property a|b holds since a|b is true in clock tick 0. t
Boolean expressions when used as Boolean properties cannot have side effects.
For example, a++ == b cannot be used as Boolean property.
Although Boolean properties are very common as part of more complex pro-
perties, Boolean properties alone can be used for specifying the initial state of the
system, as in the following example:

2 Recall that according to our definition any integral expression is also a Boolean.