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.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
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 of Lecture Notes in Computer Science. Springer-Verlag, 1990.
R. J. R. Back and R. Kurki-Suonio. Decentralization of process nets with centralized control. In Proc. 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. of PROCOMET'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. In Bulletin 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. Sere Stepwise 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
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
DOI: https://doi.org/10.1007/3-540-60117-1_9
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