Information Technology Reference
In-Depth Information
A
module M
is an tuple (
i, o, Conf , conf
0
,p, out, next
), where
-
i
is a finite set of
input ports
,
-
o
is a finite set of
output ports
,
-
Conf
is a finite set of
configurations
,
-
conf
0
∈
Conf
is the
initial configuration
,
-
p
:
Conf
VA
) is a function. For a configuration
conf
and value
assignment
σ
,
p
(
conf
)
σ
is an extension of
σ
(or is identical to
σ
),
-
out
:
Conf
→
(
VA
→
(
i
V
) is a function which, for a given con-
figuration and a given value assignment to the input ports, gives the value
assignment for the output ports, and
-
next
:
Conf
×
→
V
)
→
(
o
→
(
i
Conf
is a function, which for a given configuration
and a given value assignment to the input ports, gives the next configuration.
The set of values
V
is a finite set for a given system, i.e. there is a finite number
of value assignments to the ports. Therefore, the components for a module ex-
cluding
p
are the components of a standard Mealy automaton. The function
p
is,
as we shall see later, needed in order to describe parallel composition of modules,
where values to some input ports may be computed by other components.
×
→
V
)
→
3.1 Top-Level Modules
A “running module”
M
=(
i, o, Conf , conf
0
,p, out, next
), also called a
top-level
module
, will be given a semantics in terms of a transition system. We shall
describe the
computations
of
M
by a
transition system
,
T
S
, with initial configu-
ration
conf
0
,where
(
i
T
S
⊆
Conf
×
→
V
)
×
(
o
→
V
)
×
Conf .
σ
i
,σ
o
−→
M
conf
as an abbreviation for (
conf ,σ
i
,σ
o
, conf
)
We use
conf
∈T
S
,and
σ
i
,σ
o
−→
M
conf
, if and only if,
we define that
conf
next
(
conf ,σ
i
)=
conf
and
out
(
conf ,σ
i
)=
σ
o
.
4
Basic Modules
A basic module will be defined as a pair consisting of a
controller
and a
datapath
.
The controller is basically a finite state machine, and the datapath consists of
input ports, output ports, signals, registers, and a set of actions. We will not
go into a concrete syntactical level like that of Gezel specifications; rather the
presentation with be based on an abstract syntax, on which we can address
well-formedness conditions such as freeness from
combinatorial loops
.
4.1
Abstract Syntax of Datapaths
A
variable signature for a datapath
consists of
-
a finite set
r
of
registers
,
-
a finite set
i
of
input ports
,
Search WWH ::
Custom Search