Back, R. J. R. and Martin, A. J. and Sere, K. (1995) An action system specification of the Caltech asynchronous microprocessor. In: Mathematics of Program Construction. Lecture Notes in Computer Science. No.947. Springer , Berlin, Heidelberg, pp. 159-179. ISBN 9783540601173. https://resolver.caltech.edu/CaltechAUTHORS:20201124-174613902
Full text is not posted in this repository. Consult Related URLs below.
Use this Persistent URL to link to this item: https://resolver.caltech.edu/CaltechAUTHORS:20201124-174613902
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.
| Item Type: | Book Section | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| Related URLs: |
| |||||||||
| Additional Information: | © Springer-Verlag Berlin Heidelberg 1995. The work reported here was supported by the Academy of Finland. | |||||||||
| Funders: |
| |||||||||
| Subject Keywords: | Action System, Parallel Composition, Procedure Call, Concurrent Program, Memory Unit | |||||||||
| Series Name: | Lecture Notes in Computer Science | |||||||||
| Issue or Number: | 947 | |||||||||
| DOI: | 10.1007/3-540-60117-1_9 | |||||||||
| Record Number: | CaltechAUTHORS:20201124-174613902 | |||||||||
| Persistent URL: | https://resolver.caltech.edu/CaltechAUTHORS:20201124-174613902 | |||||||||
| Usage Policy: | No commercial reproduction, distribution, display or performance rights in this work are provided. | |||||||||
| ID Code: | 106817 | |||||||||
| Collection: | CaltechAUTHORS | |||||||||
| Deposited By: | Rebecca Minjarez | |||||||||
| Deposited On: | 03 Dec 2020 17:45 | |||||||||
| Last Modified: | 16 Nov 2021 18:57 |
Repository Staff Only: item control page
