Abstract
A process algebraic foundation is developed, for formal analysis of
synchronous hardware designs using the commercially available
hardware design language, ELLA. The underlying semantic foundation,
which is based on input/output trace sets, is first presented through
the use of state machines. Such a representation enables direct
application of standard, fully automated, trace equivalence checking
tools. To overcome the computational limitations imposed by such
analysis methods, the input/output trace semantics is re-presented
through a synchronous process algebra, EPA. Primitive processes in
EPA denote the behaviour of primitive hardware components, such as
delays or mutliplexers, with composition operators corresponding to
the different ways in which behaviours may be built. Of particular
significance is the parallel composition operator which captures the
machinery for building networks from other components/networks.
Actions in EPA are structured and signify the state of input and
output signals. This structure, however, is abstracted by developing
an algebra for the actions. In particular, the parallel composition
on processes neatly lifts to a special product operation on actions.
The EPA representation forms a good basis for semi-automated
high-level symbolic manipulation and reasoning tools. Firstly, the
original design structure can be maintained, thus easing the problems
of feedback from tools. Secondly, the application of EPA to ELLA
enables a normal form for EPA terms. This provides a route to
tractable symbolic verification and simulation, using a state
evolution method to establish strong bisimulation properties. The
method has been successfully applied to classes of unbounded state
space systems.