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