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

22.1.2.2 Eventually Property

The property s_eventually p holds on w iff the property p holds on w i:: for some
i 0. s_eventually p is a shortcut for true s_until p. Indeed, since the property
true holds on any trace, true s_until p only checks that p eventually holds. In the
research literature, s_eventually p is usually denoted as Fp or as Þ p. Bounded

forms are described in Sect. 10.5 .

22.1.2.3 Always Property

The property always p holds on w iff the property p holds on w i:: for every i 0.
always p is a shortcut for not s_eventually not p. Indeed, p always holds iff
the fact that not p holds at some time is false. In the research literature, always p
is usually denoted as Gp or as p. Bounded forms are described in Sect. 10.5 .

22.1.2.4 Until Properties

The property p until q holds on w iff either (1) 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 ,or(2)p holds in all positions of w . p until q is a shortcut for
.p s_until q/ or always p. The remaining two properties from until family
are also simple shortcuts:

￿ p until_with q is a shortcut for p until ( p and q ) .
￿ p s_until_with q is a shortcut for p s_until ( p and q ) .
The property always p can also be directly expressed through until as
p until false . Since false never holds, p must always hold.

22.2 Formal Semantics of Sequences

Like a property, a sequence defines a language, namely, the set of words (traces) that
match the sequence. Unlike the language of a property, the language of a sequence
is finitary.

Example 22.2. Given the set of variables V Df a; b g , the sequence a[ * 2] ##1 b
defines the language f aab g over the alphabet ˙ D 2 V . aab is a shortcut for the
following traces: f a gf a gf b g , f ab gf a gf b g , f a gf ab gf b g , f a gf ba gf ab g , f ab gf ab gf b g ,
f ab gf ba gf ab g , f ba gf ab gf ab g , f ab gf ab gf ab g .

t