Information Technology Reference
In-Depth Information
4.3
Abstract Syntax for Controllers
The abstract syntax for a controller is defined on the basis of a given datapath.
The controller is essentially a deterministic finite state automaton, where a con-
sistent and complete set of actions from the datapath is executed on a transition.
Since actions are described by single assignment programs, i.e. without use of
a construct for unbounded iterations, a finite set of actions is a convenient ab-
straction for an operation which can be performed in a bounded amount of time,
such as during a clock cycle.
Each transition is guarded by a
condition
on the registers of the datapath. We
let
Cond
denote the subset of
Expr
which is generated from registers (excluding
the primed ones) and constants only, using functions and the conditional
e
?
e
1
,e
2
,
i.e. input and output ports and signals cannot occur in conditions. A condition
with value
v
(for a given value assignment to registers) is considered false if
v
= 0, and true otherwise.
A
controller
is defined by
-
a finite set of
states S
,
-
an initial state
s
0
∈
S
,and
-
asetof
transitions
T⊆
S
×
Cond
×
2
Act
×
S
,where
Act
is the set of actions
from the datapath.
We shall require that a controller is
deterministic
, i.e. for every state
s
,theset
of conditions on transitions leaving
s
are mutually exclusive and complete. Thus,
for any state and any value assignment to the registers, there is precisely one
enabled
transition with true condition leaving that state. For Gezel specifications
this comes for free due to the if-then-else construction used in connection with
conditional transitions.
Furthermore, for any (
s, c, as,s
)
,werequirethat
as
is a consistent and
complete set of actions, i.e. every output port is assigned a value when the
transition is taken.
∈T
4.4
Semantics of Basic Modules
The semantics of a basic module
B
, i.e. a well-formed controller with datapath
as defined in the previous two sections, can now be defined. To this end, let
r
0
be the value assignment where every register has the value 0.
The semantics of
B
isthetuple(
i, o, Conf , conf
0
,p, out, next
), where
-
Conf
=
S
V
),
-
conf
0
=(
s
0
,r
0
), and
-
the functions
next, out
and
p
are defined as follows: Consider an arbitrary
configuration (
s, σ
r
)andlet(
s, e, as,s
)
×
(
r
→
be the uniquely determined
transition which is enabled in that configuration, i.e. where
∈T
E
[[
e
]]
σ
r
∈{
0
,
⊥}
.
Then
p
(
s, σ
r
)
σ
=
as
(
σ
r
+
σ
)
out
((
s, σ
r
)
,σ
i
)=(
p
(
s, σ
r
)
σ
i
)
o
next
((
s, σ
r
)
,σ
i
)=(
s
, update
(
σ
r
,p
(
s, σ
r
)
σ
i
)
|
Search WWH ::
Custom Search