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

22.1.2 Derived Properties

The rest of the SVA property operators that do not operate on sequences are derived.
They can be expressed through the basic operators defined in Sect. 22.1.1 .Inthis
section, we provide the list of these operators, except for the operators if and case
because their derivation was explained in Sect. 10.2 .

22.1.2.1 Boolean Connectives

In addition to and , SVA defines the Boolean property connectives or , implies ,
and iff .

Disjunction Property: w ˆ p or q iff either w ˆ p or w ˆ q. p or q is a shortcut
notation for not ( not p and not q ) . In the research literature, p or q is usually
denoted as p _ q.

Implication Property: w ˆ p implies q iff either w 6ˆ p or w ˆ q. p implies q
is a shortcut notation for not .p or not q/. In the research literature, p implies q
is usually denoted as p ! q.
Given an assertion p, an assumption q, and a model M , it is possible to rewrite
the relation M jj q ˆ p 2 using an implication property as M ˆ q ! p. Indeed, the
first formula means that all words satisfying both M and q also satisfy p, and
the second formula means that all words satisfying M either satisfy p or do not
satisfy q.

Example 22.1. Consider the following assertion statements:
m1: assume property (a);
a1: assert property (b);
a2: assert property (a implies b);
Assertion a1 together with assumption m1 are not equivalent to assertion a2 if they
are not in the scope of an initial procedure. The reason is that assertions and
assumptions out of scope of an initial procedure are interpreted as having an
implicit outermost always operator. At module level, for example, a1 together with
m1 is equivalent to the following:
initial a3: assert property (( always a) implies ( always b));
Assertion a3 is weaker than a2 .

t

Equivalence Property: w ˆ p iff q iff either both w ˆ p and w ˆ q,or w 6ˆ p
and w 6ˆ q. p iff q is a shortcut notation for .p implies q/ and .q implies p/.
In the research literature, p iff q is usually denoted as p $ q or as p q.

2 Recall that in this context jj represents parallel composition of the two models.