Formal Semantics - SVA: The Power of Assertions in SystemVerilog - page 477

We use the following notation:
￿ w is a (finite or infinite) word, or trace, over alphabet ˙ D 2 V .
￿ Each letter in the word w is numbered by a nonnegative integer number; the i th
letter is denoted as w i . The numbering starts from 0, so that the first letter is w 0 .
￿If w is a finite word, its length is denoted as j w j .
￿ The empty word is denoted as ". The empty word does not contain any letters,
and its length is 0.
￿ w i::

is the suffix of the word w starting from the letter w i . More precisely, w i::

is

the word obtained from w by deleting its first i letters. If j w j i then w i:: D ".

￿ w i;j , where i j is the finite segment of the word w starting from the letter w i
and ending at the letter w j . More precisely, w i;j is the finite word obtained from
the word w by deleting its i first letters and also deleting all its letters after the
j C 1 st

(i.e., after the letter j ).

We also use symbolic notation for the letters. For example, assuming that V D
f a; b g , then w 0 D a ^: b means that in the first position of the word (trace) a is 1

and b is 0.
To denote that the word w satisfies the property p, we write w ˆ p. In the context
of property satisfaction, w is assumed to be infinite. Finally, we assume that all the
properties in this section are unclocked (or controlled by the global clock).

22.1.1 Basic Property Forms

We consider first basic SVA property operators: Boolean property, negation, con-
junction, nexttime , and s_until . Their formal semantics is defined recursively,
starting from the Boolean property.

22.1.1.1 Boolean Property

The Boolean property e, where e is a Boolean expression over variables in V is
satisfied on all words such that e holds on their first letter:

w ˆ e iff w 0 ! e.

w 0

! e means that if the values of the variables of V specified in w 0 are substituted
into e, then the result is true. Equivalently, w 0

! e means that this Boolean formula
is a tautology over valuations of the variables in V . In this case, we also write
w 0

ˆ e.
For example, if w 0 D a ^: b then w ˆ a, and w ˆ a _ b,but w 6ˆ a ^ b.

In what follows, we assume that we know the formal semantics of each
subproperty, and thus we define the semantics of compound properties recursively
in terms of the semantics of their components.