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

￿ or —disjunction
p or q is true iff either p or q (or both) are true.
The above definitions with obvious modifications apply also to the way property
truth is determined in clock tick i . For example, p and q is true in clock tick i iff
both p and q aretrueinclockticki .
In the special case of Boolean properties, it is possible to rewrite Boolean
property connectives in a different way. For example, e1 and e2 means that both
e1 and e2 are true, which can be also expressed as e1 && e2 . 7 The domain of the
operators && and and is different: && may be used with Boolean expressions only,
while and requires sequence or property arguments. Since Boolean expressions in
this case may also be considered as Boolean properties, both operators may be
applied to them. Note also that && has greater precedence than and .
Similarly, e1 or e2 is equivalent to e2 || e2 ,but not e is equivalent to !e
only if the property clock eventually ticks (see Chap. 22 ). 8

Example 5.16. The following expression is syntactically illegal: (a and b)|| c .
Although a and b is logically equivalent to a&&b , it is not a Boolean expression.
The operator || , however expects both its operands to be Boolean expressions. t
Example 5.17. What does not always p mean?
Solution: According to the definition of property not , this property is true iff
always p is false, which means that p is false at least in one clock tick. This is
exactly s_eventually not p . Similarly, not s_eventually p is always not p .
Discussion: For a Boolean expression e , not always e may be rewritten as
s_eventually !e and not s_eventually e as always !e .

t

Example 5.18. Reset rst must be asserted during the first two cycles.

Solution:

initial a1:
assert property (@( posedge clk) rst and nexttime rst);

Discussion: Note that rst && nexttime rst is syntactically illegal: && expects
both of its operands to be Boolean expressions, while nexttime rst is a property,
but not a Boolean expression.
A more elegant way to write the same property is described in Sect. 6.5 .

t

7 Even though && is a short circuit operator (that is, its second operand is not evaluated if the first
operand is evaluated to false), and and is not, there is no difference between them in this case,
since expressions used in assertions cannot have side effects. See Sect. 5.1 .
8 The difference may not be observable in simulation depending on whether the simulator takes
into account the strength of properties at the end of simulation. not e is a strong property, while
!e is weak.