Hardware Reference
In-Depth Information
w
;L
0
ˆ
weak
(
r
)
iff for every 0
j<
j
w
j
,
w
0;j
!
;L
0
ˆ
strong
(
r
)
. r must
>
not admit an empty match.
w
;L
0
ˆ
r
|->
p iff for every 0
j<
j
w
j
and L such that
N
w
0;j
;L
0
;L
j
r ,
w
j::
;L
ˆ
p.
w
;L
0
ˆ
p
or
q iff either
w
;L
0
ˆ
p or
w
;L
0
ˆ
q.
w
;L
0
ˆ
p
and
q iff both
w
;L
0
ˆ
p and
w
;L
0
ˆ
q.
w
;L
0
ˆ
nexttime
p iff either
j
w
jD
0 or
w
1::
;L
0
ˆ
p.
w
;L
0
ˆ
p
s_until
q iff there exists 0
j<
j
w
j
such that
w
j::
;L
0
ˆ
q and
for every 0
i<j,
w
i::
;L
0
ˆ
p.
w
;L
0
ˆ
accept_on
(
b
)
p iff either
-
w
;L
0
ˆ
p and no letter of
w
satisfies b,or
-forsome0
i<
j
w
j
,
w
i
!
;L
0
ˆ
p.
8
It is worth noting that in the rule for
|->
, the intermediate local variable context
L is universally quantified. This is how the formal semantics specifies that multiple
matches over the same interval that result in distinct values of the local variables
must be treated as separate matches, each obligating a check of the consequent with
the corresponding local variable values.
ˆ
b and
w
0;i
1
>
22.7
Formal Semantics of Recursive Properties
This section gives a brief description of the formal semantics of recursive properties.
The main idea is to define the semantics of a recursive property in terms of the
semantics of associated non-recursive properties. Intuitively, these non-recursive
properties are approximations to greater and greater depth of the unrolling of the
recursion. There is some subtlety to the definition because recursive properties may
instantiate non-recursive properties and vice versa. This section presumes that the
semantics of instantiation of non-recursive properties is understood, at least at the
intuitive level of substituting actual arguments for formal arguments, while avoiding
aliasing that is contrary to the rules of name resolution. For further discussion, see
Annex F.4 of the LRM.
First, let us say more precisely what constitutes a recursive property and a
recursive instance. Consider the source code for a SystemVerilog model. Within
it are finitely many declarations of named properties and finitely many instances
of named properties. The
dependency digraph
is the directed graph
h
V; E
i
formed
as follows. The node set V consists of the named properties that appear in the
source code. Each named property has a unique name, where the name may be
expanded as a hierarchical name, e.g., as needed for disambiguation. If p and q are
two named properties, then there is a directed edge from p to q in the edge set E
iff there is an instance of q within the declaration of p. A named property is said
8
In case i
D
0,
w
0;
1
is understood to denote the empty word.
Search WWH ::
Custom Search