A process-algebraic approach to the design of asynchronous (counterflow) pipelines

In this paper we discuss the use of an approach in the design and verification of an asynchronous processor, the Sproull Counterflow Pipeline Processor Architecture (SCPP-A). As is often the case, the formal specification of the problem turns out to be the more difficult part. Once in the formal framework, we are in the realm of algebraic manipulations, where verification is a matter of proving theorems. We show how we break down such an asynchronous specification into a pipeline of stages interleaved with arbitration elements, the so-called Cops. Due to space limitations we confine ourselves to the topmost specifications, and refrain from decomposing the Stage and Cop any further