An action system specification of the caltech asynchronous microprocessor

  • R. J. R. Back
  • A. J. Martin
  • K. Sere
Contributed Lectures
Part of the Lecture Notes in Computer Science book series (LNCS, volume 947)


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.


Action System Parallel Composition Procedure Call Concurrent Program Memory Unit 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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.Google Scholar
  2. 2.
    R. J. R. Back. Procedural abstraction in the refinement calculus. Technical Report, Åbo Akademi University, Department of Computer Science. Turku, Finland 1987.Google Scholar
  3. 3.
    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.Google Scholar
  4. 4.
    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.Google Scholar
  5. 5.
    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.Google Scholar
  6. 6.
    R. J. R. Back and K. Sere. Stepwise refinement of parallel algorithms. Science of Computer Programming 13, pages 133–180, 1989.Google Scholar
  7. 7.
    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.Google Scholar
  8. 8.
    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.Google Scholar
  9. 9.
    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.Google Scholar
  10. 10.
    K. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.Google Scholar
  11. 11.
    E. W. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976.Google Scholar
  12. 12.
    N. Francez. Cooperating proofs for distributed programs with multiparty interactions. Information Processing Letters, 32:235–242, 1989.Google Scholar
  13. 13.
    T. Kuusela, J. Plosila, R. Ruksenas, K. Sere, and Zhao Yi. Designing delay-insensitive circuits within the action systems framework. Manuscript, 1995.Google Scholar
  14. 14.
    A. J. Martin. Synthesis of Asynchronous VLSI Circuits. CalTech, Technical Report, 1993.Google Scholar
  15. 15.
    C. C. Morgan. The specification statement. ACM Transactions on Programming Languages and Systems, 10(3):403–419, July 1988.Google Scholar
  16. 16.
    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.Google Scholar
  17. 17.
    J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9:287–306, 1987.Google Scholar
  18. 18.
    K. Sere Stepwise Refinement of Parallel Algorithms. PhD thesis, Department of Computer Science, Åbo Akademi University, Turku, Finland, 1990.Google Scholar
  19. 19.
    J. Staunstrup and M. R. Greenstreet. Synchronized Transitions. IFIP WG 10.5, Summer school on Formal Methods for VLSI Design, Lecture Notes 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • R. J. R. Back
    • 1
  • A. J. Martin
    • 2
  • K. Sere
    • 3
  1. 1.Department of Computer ScienceÅbo Akademi UniversityTurkuFinland
  2. 2.Department of Computer ScienceCalifornia Institute of TechnologyPasadenaUSA
  3. 3.Department of Computer Science and Applied MathematicsUniversity of KuopioKuopioFinland

Personalised recommendations