Abstract
This work develops a process algebra called EPA which is suitable
for representing the semantics of synchronous hardware systems.
EPA is similar to CCS/SCCS but
supports simultaneous input/output of value expressions via
labelled channels, and provides value-passing between process terms. A
specialised product operation gives synchronous communication between
processes.
A special normal form, using a subset of EPA, provides the basis
for (symbolic) simulation and verification tools. A novel state
bisimulation rule is introduced, an extension of standard
bisimulation,
which offers an efficient mechanism called state evolution
for comparing the behaviour of process terms at an abstract level.
The soundness of the rule with respect to (standard) bisimulation is shown.