Hardware Reference
In-Depth Information
our approach). Simulation relations in general are stronger (more restrictive) than
language containment, i.e., a simulation relation implies language containment, but
not vice versa.
The use of simulation relation instead of language containment avoids de-
terminization and leads to an algorithm of polynomial complexity bounded by
O.
j
S
A
j
:
j
S
C
j
:
j
T
A
j
:
j
T
C
j
/,where
j
S
A
j
(
j
S
C
j
) is the number of states of M
A
(M
C
)and
j
T
A
j
(T
C
) is the size of the transition relation of M
A
(M
C
). In [12] a solvability
condition is given, based on the notion of simulation relation between the automata
which generate the possible output sequences produced by an FSM. Model matching
was investigated also within the frame of supervisory control in [8], relying on the
relation between the controllability of a language and a given bisimulation; the same
formulation was adopted in [91], where an implicit representation of automata based
on algebraic methods is proposed.
Notice that for some topologies, like the rectification topology, solutions based
on simulation relations do not provide the complete flexibility.
5.1.9
Structural Replacement of Synchronous and Asynchronous
Hardware
We list a few lines of investigation covering topics that arise from structural
replacement, when the implementability of a legal behavior is considered:
1. Model matching of asynchronous sequential machines. Issues of races, infinite
cycles and adversarial inputs were discussed in [47, 99, 106, 133, 146].
2. Replacement and verification of hierarchical models of synchronous and asyn-
chronous circuits. Trace theory has been used by Dill [35] to model hierarchical
verification of asynchronous hardware. E. Wolf developed it further in [22, 145]
to derive a closed-form expression that specifies all and only the permissible
replacement circuitry in a given location in a circuit or partially-structured
specified model. Her frame applies to both combinational circuits and clocked
sequential circuits. Nondeterministic specifications are allowed too. The circuit
semantics adopted allows the expression of circuits that contain unlatched
feedback loops, and therefore, among the degrees of freedom available for the
correct implementation of a part of a logic network, there is the possibility that it
contains unlatched feedback.
3. Safe replaceability. It is the problem of replacing components when there
is limited or no information on the initial states of the component under
replacement, After the pioneering work of C. Pixley, important contributions
came from Singhal and Brayton [58, 88, 127-129].
Search WWH ::
Custom Search