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

Table 5.1 Basic property

Operator Associativity
not -
nexttime -
and Left
or Left
until Right
until_with Right
always -
s_eventually -

operators

We describe only the elementary and most commonly used property operators
here. The less frequently used and more complex operators are discussed in
Chap. 10 .
In this chapter, we use the following convention: letters a , b , c , and, e denote
integral expressions or signals; p and q denote properties. All letters may be
optionally indexed. We enumerate clock ticks with integer numbers starting with 0.
In the diagrams, we mark the ticks where a Boolean expression holds with a black
dot, and the ticks where a property holds with a black triangle.
The property operators described in this chapter are summarized in Table 5.1 .
They are grouped by their precedence, from highest to lowest.
Properties can be built from simpler properties in a recursive manner. First we
define “primitive” properties, and then we show how to build new properties using
property operators from existing ones. The primitive properties are constructed from
sequences. However, the notion of a sequence is less intuitive before introducing the
notion of a property. Therefore, in this chapter we consider a Boolean, which is the
simplest form of sequence, as the primitive form, and postpone the introduction of
sequences until Chap. 6 . In Chap. 6 , we clarify why primitive properties are in fact
sequential properties and that Boolean properties are the simplest case of sequential
properties.

Example 5.1. To illustrate what we mean by recursive definition of properties,
consider property nexttime always e , the meaning of which is explained later.
This property is built by applying property operator nexttime to the simpler
property always e . The latter property, in its turn, is built by applying property
operator always to the primitive property e .

t

5.1 Boolean Property

The simplest property is a Boolean property —an integral expression e , which is
treated as Boolean. A Boolean expression is true if it has at least one bit set to 1,
and false otherwise, i.e., when all its bits have values 0, x or z . Now, extending the
meaning, we define a Boolean property informally for a point on a trace as follows: