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.