Part of the book series:Lecture Notes in Computer Science ((LNCS,volume 947))
Included in the following conference series:
197Accesses
Abstract
The action system framework for modelling parallel programs is used to formallyspecify a microprocessor. First the microprocessor is specified as a sequential program. The sequential specification is thendecomposed andrefined 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 ofspatial 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 forformal VLSI circuit design.
This is a preview of subscription content,log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. J. R. Back.On the Correctness of Refinement Steps in Program Development. PhD thesis, Department of Computer Science, University of Helsinki, Helsinki, Finland, 1978. Report A-1978-4.
R. J. R. Back.Procedural abstraction in the refinement calculus. Technical Report, Åbo Akademi University, Department of Computer Science. Turku, Finland 1987.
R. J. R. Back. Refinement calculus, part II: Parallel and reactive programs. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors,Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness. Proceedings. 1989, volume 430 ofLecture Notes in Computer Science. Springer-Verlag, 1990.
R. J. R. Back and R. Kurki-Suonio. Decentralization of process nets with centralized control. InProc. of the 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, pages 131–142, 1983.
R. J. R. Back, A. J. Martin, and K. Sere.Specification of a Microprocessor. Technical Report, Åbo Akademi University, Department of Computer Science. Ser. A, No 148, Turku, Finland 1992.
R. J. R. Back and K. Sere. Stepwise refinement of parallel algorithms.Science of Computer Programming 13, pages 133–180, 1989.
R. J. R. Back and K. Sere. Action systems with synchronous communication. Proc. ofPROCOMET'94, San Miniato, Italy, June 1994. E.-R. Olderog, editor,Programming Concepts, Methods and Calculi, IFIP Transactions A-56, pages 107–126, North-Holland 1994.
R. J. R. Back and K. Sere. From modular systems to action systems.Proc. of Formal Methods Europe'94, Spain, October 1994.Lecture Notes in Computer Science. Springer-Verlag, 1994.
J. Bowen et al.. A ProCoS II Project Description: ESPRIT Basic Research project 7071. InBulletin of the EATCS, volume 50, pages 128–137, June 1993.
K. Chandy and J. Misra.Parallel Program Design: A Foundation. Addison-Wesley, 1988.
E. W. Dijkstra.A Discipline of Programming. Prentice-Hall International, 1976.
N. Francez. Cooperating proofs for distributed programs with multiparty interactions.Information Processing Letters, 32:235–242, 1989.
T. Kuusela, J. Plosila, R. Ruksenas, K. Sere, and Zhao Yi. Designing delay-insensitive circuits within the action systems framework. Manuscript, 1995.
A. J. Martin. Synthesis of Asynchronous VLSI Circuits.CalTech, Technical Report, 1993.
C. C. Morgan. The specification statement.ACM Transactions on Programming Languages and Systems, 10(3):403–419, July 1988.
C. C. Morgan, K. A. Robinson, and P. H. B. Gardiner.On the Refinement Calculus. Technical Monograph PRG-70, Programming Research Group, Oxford University, October 1988.
J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus.Science of Computer Programming, 9:287–306, 1987.
K. SereStepwise Refinement of Parallel Algorithms. PhD thesis, Department of Computer Science, Åbo Akademi University, Turku, Finland, 1990.
J. Staunstrup and M. R. Greenstreet.Synchronized Transitions. IFIP WG 10.5, Summer school on Formal Methods for VLSI Design, Lecture Notes 1990.
Author information
Authors and Affiliations
Department of Computer Science, Åbo Akademi University, FIN-20520, Turku, Finland
R. J. R. Back
Department of Computer Science, California Institute of Technology, 91125, Pasadena, CA, USA
A. J. Martin
Department of Computer Science and Applied Mathematics, University of Kuopio, FIN-70211, Kuopio, Finland
K. Sere
- R. J. R. Back
You can also search for this author inPubMed Google Scholar
- A. J. Martin
You can also search for this author inPubMed Google Scholar
- K. Sere
You can also search for this author inPubMed Google Scholar
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Back, R.J.R., Martin, A.J., Sere, K. (1995). An action system specification of the caltech asynchronous microprocessor. In: Möller, B. (eds) Mathematics of Program Construction. MPC 1995. Lecture Notes in Computer Science, vol 947. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60117-1_9
Download citation
Published:
Publisher Name:Springer, Berlin, Heidelberg
Print ISBN:978-3-540-60117-3
Online ISBN:978-3-540-49445-4
eBook Packages:Springer Book Archive
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative