CaltechAUTHORS
  A Caltech Library Service

An action system specification of the Caltech asynchronous microprocessor

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:
URLURL TypeDescription
https://doi.org/10.1007/3-540-60117-1_9DOIArticle
https://rdcu.be/cbCpQPublisherFree ReadCube access
Additional Information:© Springer-Verlag Berlin Heidelberg 1995. The work reported here was supported by the Academy of Finland.
Funders:
Funding AgencyGrant Number
Academy of FinlandUNSPECIFIED
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