An action system specification of the Caltech asynchronous microprocessor
- Creators
- Back, R. J. R.
- Martin, A. J.
- Sere, K.
- Other:
- Möller, Bernhard
Abstract
The action system framework for modelling parallel programs is used to formally specify a microprocessor. First the microprocessor is specified as a sequential program. The sequential specification is then decomposed and refined into a concurrent program using correctness-preserving program transformations. Previously this microprocessor has been specified in a semi-formal manner at Caltech, where an asynchronous circuit for the microprocessor was derived from the specification. We propose a specification strategy that is based on the idea of spatial decomposition of the program variable space. Applying this strategy we give a completely formal derivation of a high level specification for the Caltech microprocessor. We also demonstrate the suitability of action systems and the stepwise refinement paradigm for formal VLSI circuit design.
Additional Information
© Springer-Verlag Berlin Heidelberg 1995. The work reported here was supported by the Academy of Finland.Additional details
- Eprint ID
- 106817
- DOI
- 10.1007/3-540-60117-1_9
- Resolver ID
- CaltechAUTHORS:20201124-174613902
- Academy of Finland
- Created
-
2020-12-03Created from EPrint's datestamp field
- Updated
-
2021-11-16Created from EPrint's last_modified field
- Series Name
- Lecture Notes in Computer Science
- Series Volume or Issue Number
- 947