Formal design of a class of computers — its high stage: abstract microprogramming

  • Li -Guo Wang
  • Michael Mendler
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 987)


We present a novel construction model of hardware and demonstrate how to use it in the entire process of formally designing a class of computers involving their specification, construction, and verification. In this paper we focus on the high stages of the design: the refinement from the behaviour specification at machine instruction level to the abstract microprogram at the term transition level. The concept of term transition introduced in this paper establishes a new generic high-level design stage which is common for computer architecture and design. Our approach is based on formal syntax and formal proof and constitutes a framework for the rigorous specification and verification of hardware synthesis systems.


Construction Model Specification Scheme Formal Design Abstract Syntax Machine Instruction 
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.


  1. [1]
    Simon Bainbridge, Albert Camilleri and Roger Fleming, Theorem Proving as an Industrial Tool for System Level Design. In [34], pp. 253–276.Google Scholar
  2. [2]
    David A. Basin, Geoffrey M. Brown, and Miriam E. Leeser, Formally verified synthesis of combinational CMOS circuits. In L. J. M. Claesen, editor, Formal VLSI Specification and Synthesis, page 197–206, North-Holland, 1990.Google Scholar
  3. [3]
    D. A. Basin, Extracting Circuits from Constructive Proofs. In 1991 International Workshop on Formal Verification in VLSI Design. ACM IFIP WG 10.2, Jan. 1991.Google Scholar
  4. [4]
    G. Birtwistle and P. Subrahmanyam, eds., VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers, Boston, 1988.Google Scholar
  5. [5]
    J. Bormann, H. Nusser-Wehlan, and G. Venzl, Formal Design in an Industrial Research Laboratory: Lessons and Perspectives. In J. Staunstrup and R. Sharp, eds., Designing Correct Circuits, North-Holland, 1992.Google Scholar
  6. [6]
    D. Borrione, H. Collavizza and C. Le Faou, ΜSPEED: A Framework for Specifying and Verifying Microprocessors. In Formal Methods in VLSI Design, Springer, 1991.Google Scholar
  7. [7]
    B. Bose and S. D. Johnson, DDD-FM9001: Derivation of a Verified Microprocessor. In [30].Google Scholar
  8. [8]
    K. M. Chandy and J. Mishra, Parallel Program Design. A Foundation. Addison Wesley, 1988.Google Scholar
  9. [9]
    L. Claesen, editor, IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Volume 1+2, Elsevier/North-Holland, 1989.Google Scholar
  10. [10]
    Avra Cohn, A Proof of Correctness of the Viper Microprocessor: First Level. In [4], pp. 27–71.Google Scholar
  11. [11]
    Avra Cohn, Correctness Properties of the Viper Block Model: The Second Level. In G. Birtwistle and P. Subrahmanyam, eds., Current Trends in Hardware Verification and Automated Theorem Proving, Springer-Verlag, 1989, pp.1–91.Google Scholar
  12. [12]
    M. P. Fourman, R. L. Harris, Lambda-Logic and Mathematics Behind Design Automation, 26th ACD/IEEE Design Automation Conference, 1988.Google Scholar
  13. [13]
    M. P. Fourman, Formal System Design. In [33], pp 191–236.Google Scholar
  14. [14]
    Gopalakrishnan, Genesh and Fujimoto, Richard, Design and Verification of the Rollback Chip Using HOP: a Case Study of Formal Methods Applied to Hardware Design. ACM Transactions on Computer Systems, Vo. 11 No. 2 pp. 109–145, May 1993.Google Scholar
  15. [15]
    M. J. C. Gordon, Proving a Computer Correct with the LCF-LSM Hardware Verification System. Technical Report No. 42, Computer Laboratory, University of Cambridge, 1983.Google Scholar
  16. [16]
    M. J. C. Gordon, Why higher-order logic is a good formalism for specifying and verifying hardware. in: G. Milne and P. Subrahmanyam, eds., Formal Aspects of VLSI Design, North-Holland, 1986, pp. 153–177.Google Scholar
  17. [17]
    M. J. C. Gordon, HOL: A Proof Generating System for Higher-Order Logic. University of Cambridge, Computer Laboratory, Tech Report No. 103, 1987.Google Scholar
  18. [18]
    F.K. Hanna and N.Daeche, Specification and Verification of Digital Systems using Higher-Order Predicate Logic. IEE Proceedings, Vol. 133, Part E, No. 5, September 1986, pp. 242–254.Google Scholar
  19. [19]
    F.K. Hanna, M. Longley, and N. Daeche, Formal synthesis of digital systems. In [9], pages 532–548.Google Scholar
  20. [20]
    F.K. Hanna and N.Daeche. Strongly-Typed Theory of Structure and Behaviors. In [30], pp. 39–54.Google Scholar
  21. [21]
    N.A. Harman and J. V. Tucker, Algebraic Models and the Correctness of Microprocessors. In [30], pp. 92–108.Google Scholar
  22. [22]
    Warren A. Hunt, FM8501, A Verified Microprocessor. Ph.D. Thesis, Report No. 47, Institute for Computing Science, University of Texas, Austin, December 1985.Google Scholar
  23. [23]
    P.B. Jackson, Nuprl and its Use in Circuit Design. In [34], pp. 311–336.Google Scholar
  24. [24]
    G. Jones and M. Sheeran, Circuit Design in Ruby. In [33].Google Scholar
  25. [25]
    M. Langevin and E. Cerny, Verification of Processor-like Circuits. In Advanced Work on. Correct Hardware Design Methodology, Turin, 12–14 June 1991.Google Scholar
  26. [26]
    J. J. Joyce, G. Birtwistle and M. Gordon, Proving a Computer Correct in Higher Order Logic. Report No. 100, Computer Laboratory, Cambridge University, 1986.Google Scholar
  27. [27]
    Mahmood, M. and Mavaddat, F. and Elmasry, M.I. and Cheng, M.H.M, A Formal Language Model of Logic Microcode Synthesis. In [9], pp. 21–39.Google Scholar
  28. [28]
    Thomas F. Melham, Abstraction mechanism for hardware verification. In G. Birtwistle and P.A. Subrahmanyam, eds., VLSI Specification, Verification, and Synthesis, pages 267–291. Kluwer Academic Publishers, 1988.Google Scholar
  29. [29]
    G. J. Milne, Design for Verifiability. In Hardware Specification, Verification and Synthesis: Mathematical Aspects, Cornell University, USA, July 1989.Google Scholar
  30. [30]
    G. J. Milne and L. Pierre, eds., Correct Hardware Design and Verification Methods, LNCS 683, Springer-Verlag, May 1993.Google Scholar
  31. [31]
    Lawrence C. Paulson. Isabelle Tutorial and User's Manual, 1990.Google Scholar
  32. [32]
    J. Staunstrup, A Formal Approach to Hardware Design. Kluwer Academic Publishers, 1994.Google Scholar
  33. [33]
    J. Staunstrup, editor, IFIP WG 10.5 Formal Methods for VLSI Design, North-Holland, 1990.Google Scholar
  34. [34]
    V. Stavridou, T.F. Melham, and R.T. Boute, eds., Theorem Provers in Circuit Design: Theory, Practice and Experience. IFIP TC10/WG 10.2, North Holland, June 1992.Google Scholar
  35. [35]
    V. Stavridou, J. A. Goguen, A. Stevens, S. M. Eker, S. N. Alonefits, and K. M. Hobley, FUNNEL and 2OBJ: Towards and Integrated Hardware Design Environment. In [34].Google Scholar
  36. [36]
    Dany Suk, Hardware Synthesis in Constructive Type Theory. In G. Jones and M. Sheeran, eds., Designing Correct Circuits, pp 29–49, Oxford, Springer-Verlag, 1990.Google Scholar
  37. [37]
    Li-Guo Wang, Deriving a Correct Computer. In L. J. M. Claesen and M. J. C. Gordon, eds., Higher Order Logic Theorem Proving and its Application, pages 449–458, Elsevier/North-Holland, 1993.Google Scholar
  38. [38]
    Li-Guo Wang, Formal Derivation of A Class of Computers. PhD Thesis, LFCS, Department of Computer Science, University of Edinburgh, Oct. 1994.Google Scholar
  39. [39]
    P. J. Windley, A Hierarchical Methodology for the Verification of Microprogrammed Microprocessors. In IEEE Symposium on Security and Privacy, May 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Li -Guo Wang
    • 1
  • Michael Mendler
    • 2
  1. 1.Department of Computer ScienceUniversity of EdinburghUK
  2. 2.Department of Computer ScienceTechnical University of DenmarkDenmark

Personalised recommendations