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

22.1.1.2 Negation Property

The property not p holds on w iff the property p does not hold on w :

w ˆ not p iff w 6ˆ p:

In the research literature, not p is usually denoted as : p. We continue the
discussion on the formal semantics of negation in Sect. 22.3.4 .

22.1.1.3 Conjunction Property

The property p and q holds on w iff both properties p and q hold on w :

w ˆ p and q iff w ˆ p and w ˆ q:

In the research literature, p and q is usually denoted as p ^ q.

22.1.1.4 Nexttime Property

The property nexttime p holds on w iff the property p holds on w 1:: :

w ˆ nexttime p iff w 1::

ˆ p

In the research literature, nexttime p is usually denoted either as Xp or as p.
Derived forms of this property are described in Sect. 10.5 .

22.1.1.5 Strong Until Property

The property p s_until q holds on w iff there exists i 0 such that p holds in all
positions of w up until, but not including, position i , and q holds in position i :

w ˆ p s_until q iff there exists i so that w i ˆ q and for every 0 j<i, w j:: ˆ p.

In the research literature, p s_until q is usually denoted 1

as pUq.

1 In the research literature, the operator s_until is called simply until , and the operator until
is called weak until .