Case study: Specification and refinement of the PI-Bus

Abstract

The Peripheral Interconnect Bus (PI-Bus) is part of the Open Microprocessor systems Initiative, which is in the process of setting standards for a wide range of chip components, so as to guarantee compatibility between components from different vendors. One of the problems arising in the standardization effort is that the standard needs to be as definite as possible without prejudicing implementation issues. This paper presents a formalisation of the draft standard for the PI-Bus which suggests that this problem has not yet been adequately addressed. We use CSP to give a high-level specification which corresponds to the compulsory aspects of the draft standard, and show that there are two implementations which are both valid refinements of the specification, but are mutually incompatible.

Explicit timing events are used to bound to the nearest clock phase the time at which a communication event may happen and avoid the necessity to reason in a fully timed semantics. There is, however, a slight deviation from standard CSP in that choice between communication and timing events is prioritised towards the former. This means that a process will perform a communication event rather than a timing event whenever it has the choice.

funded by Esprit Project 7267/ OMI-Standards