SPECIFYING THE CALTECH ASYNCHRONOUS MICROPROCESSOR

The action systems framework for modelling parallel programs is used t o formally specify a microprocessor. First the microprocessor is speci fied as a sequential program. The sequential specification is then dec omposed and refined into a concurrent program using correctness-preser ving program transformations. Previously this microprocessor has been specified at Caltech, where an asynchronous circuit for the microproce ssor was derived from the specification. We propose a specification st rategy that is based on the idea of spatial decomposition of the progr am variable space.