Information Technology Reference
In-Depth Information
An action (
an,p
) (and a single assignment program
p
) is called
well-formed
if
the dependency graph
≺
p
is acyclic, and has input ports only as its sources. All
variables of
≺
p
, which are not input ports, are called
assigned variables
.Wecall
such dependency graphs for well-formed.
A
datapath
consists of a finite set
Act
=
{
(
an
1
,p
1
)
,...,
(
an
n
,p
n
)
}
of well-
formed actions with unique names, i.e.
an
i
=
an
j
implies
i
=
j
.
By the
signature for the actions
we understand an association of the appro-
priate dependency graph:
graph(
an
i
)=
≺
p
i
,
with every action name.
We shall call a subset
as
of action names for
consistent
,
if the corresponding dependency graphs have disjoint sets of assigned variables.
For a consistent set of action names, the single assignment program obtained
by joining all single assignment programs of the elements, will be a well-formed
single assignment program.
Furthermore,
as
is called
complete
if every output port is an assigned variable
of some dependency graph of an element in
as
.
⊆{
an
1
,...,an
n
}
4.2
Semantics of Datapaths
In order to define the meaning of a datapath, we must define the meaning of
variables, expressions and actions.
We assume that
F
is an assignment of a function:
f
n
∈ V
n
→ V,
with every
n
-ary function symbol
f
n
∈
F
.Furthermore,let
V
⊥
=
V
∪{⊥}
,where
⊥
is a special element denoting undefined.
Semantics of Expressions:
The semantics of an expression
e
is a function:
E
[[
e
]]
∈
VA
→
V
⊥
, defined inductively as follows:
E
[[
c
]]
σ
=
c
=
σ
(
x
) f
x
∈
dom
σ
E
[[
x
]]
σ
⊥
otherwise
[[
f
n
(
e
1
,...,e
n
)]]
σ
=
f
n
(
v
1
,...,v
n
) f
⊥
=
v
i
=
E
[[
e
i
]]
σ
,for
i
=1
,...n
E
⊥
otherwise
⎧
⎨
E
[[
e
2
]]
σ
if 0 =
E
[[
e
]]
σ
E
[[
e
1
]]
σ
E
[[
e
]]
σ
∈
V
E
[[
e
?
e
1
,e
2
]]
σ
=
if 0
=
⎩
⊥
otherwise.
Semantics of Single Assignment Programs and Actions:
Aviewofa
well-formed single-assignment program
p
is that it maps value assignments for
Search WWH ::
Custom Search