Information Technology Reference
In-Depth Information
-
a finite set
o
of
output ports
,and
-
a finite set
s
of
local signals
.
Registers are special in the sense that they keep their values throughout a
clock cycle, and a register will keep its value from one cycle to the next if the
register is not changed. Therefore, we introduce a new variable
r
for the next
value of every register
r
r
.Let
r
=
r
|
∈
{
r
∈
r
}
be the set of these “primed
variables”.
These five sets are assumed to be mutually exclusive, and we shall use the
term
variable
for an element of one of these sets:
i
r
∪
Var
=
r
∪
∪
o
∪
s.
V
be a set of constants, and
F
a set of function symbols equipped
with
arities
. Then, the set of expressions
e
Let
C
⊆
Expr
is generated from constants
and variables using functions and a kind of McCarthy conditional, as expressed
in the following abstract grammar:
∈
e
::=
c
|
x
|
f
n
(
e
1
,...,e
n
)
|
e
?
e
1
,e
2
,
Var /r
,and
f
n
where
c
F
is an
n
-ary function symbol. Notice that
primed registers cannot occur in expressions.
For a given variable signature, an
action
is a pair (
an,p
), where
an
is the
name of the action and
p
is a
single assignment program
, where registers, output
ports and signals only can be assigned a value. We shall model
p
as a partial
mapping from
r
∈
C, x
∈
∈
∪
o
∪
s
to
Expr
:
p ∈
(
r ∪ o ∪ s
)
−→
Expr .
We shall consider
p
a set of equations, which defines values for output ports,
signals and next values for registers on the basis of values for input ports and
previous values for registers.
If
p
(
x
)=
e
, then the
associated equation
is
x
=
e
if
x
is not a register,
x
=
e
if
x
is a register. Let
eqs
p
be
the set of equations associated with p
.Weshall
occasionally omit the subscript
p
when it is easily derivable from the context.
We shall now define the
dependency graph
of variables in a single-assignment
program
p
in order to formalize a well-formedness condition expressing that there
is no circular definition of variables in
p
.Intuitively,
y depends on x
,ifthevalue
of
x
is must be computed in the computation of a value for
y
. The dependency
graph for
p
, denoted by
, is a subset of (
i
(
r
∪
≺
p
or just
≺
∪
o
∪
s
)
×
o
∪
s
)and
it is defined as the set of pairs (
x, y
)forwhich:
y
=
e
∈
eqs
p
and
x
occurs in
e.
.
Constants do not occur the in the graph (their values are always present),
neither do the variables for the previous values of registers (i.e. those occurring
at the right-hand sides of equations), because these values are always known.
We shall write
x
≺
y
if (
x, y
)
∈≺
Search WWH ::
Custom Search