An experiment in high level language microprogramming and verification

Abstract

The STRUM system was created to apply software engineering techniques to microprogramming. It provides the tools that allow the microprogrammer to use high level language, structured programming, and formal program verification to create emulations for a horizontally microprogrammed computer. This system is evaluated in two parts: (1) High level microprogramming language design and its use in structured microprogramming; and (2) Verification of a large microprogram. Both parts of this evaluation include experimental results. Part I includes a comparison of an emulation created using traditional techniques to the same emulation created using the STRUM system. Part II describes the formal verification of a 1700 line program that was immediately subjected to extensive testing. This work provides new results on the efficiency of high level microprogramming languages, the effectiveness of peephole optimization for microcode and the practicality of formal microprogram verification.

References

1. 1 ACM SIGPLAN Notices. Proc. SIGPLAN/SIGMICRO Interface Meeting, Harriman, NY, May 30-June 1, 1973.9, 8 (Aug. 1974).
2. 2 Agrawala, T. Microprogramming optimization: A survey. IEEE Trans. on Computers, Special Issue on Microprogramming, (Oct. 1976), 962-973.
3. 3 Beyers, J.W., Dohse, L. J., Fucetola, J. P., Kochis, R. L., Lob, C. G., Taylor, G. L., and Zeller, E. R. A 32b VLSI CPU chip, Proc. IEEE Inter. Solid-State Circuits Conf., New York, N.Y., Feb. 1981, pp. 104-105.
4. 4 Bell, C.G. and NeweU, A., Computer Structures: Readings and Examples, McGraw Hill, New York, 1971.
5. 5 Birman, A., On proving correctness of microprograms. IBM J. Res. Develop., 18, 5, (May 1974) 250-256.
6. 6 Carter, W.C., Joyner, W.H., Jr., and Brand, D. Microprogram verification considered necessary. Proc. of the NCC, Anaheim, California, June 1978, p. 657.
7. 7 Cottrell, J.R., A verification condition generator for a structured microprogramming language. UCLA-ENG-7606, Dept of Computer Sci, University of California, Los Angeles, Los Angeles, California, Mar. 1976.
8. 8 Davidson, S. and Shriver, B.D., An overview of firmware engineering. Computer 11, 5, (May 1978) 21-33.
9. 9 Fisher, J., The Optimization of Horizontal Microcode: Within Basic Blocks and Beyond, Ph.D. Thesis, Courant Institute, New York University, New York, N.Y., 1979.
10. 10 Mathematical Aspects of Computer Science. J.T. Schwatrz, Ed. 19 (AMS, New York, 1967) pp 19-32.
11. 11 Gerhart, S.L. and Yelowitz, L., Observations of fallibility in applications of modern program methodologies. IEEE Trans. on Software Engineering, SE-2, 3, (Sept. 1976) 195-207.
12. 12 Guha, R.K., Dynamic microprogramming in a timesharing environment. Proc. 10th Ann. Workshop on Microprogramming. Niagara Falls, N.Y., October 1977, pp. 55-60.
13. 13 Hearn, A.C., REDUCE 2: A system and language for algebraic manipulation, Proc. 2nd Symp. Symbolic and Algebraic Manipulation, ACM, Los Angeles, CA; March 23-25, 1971, pp. 128-133.
14. 14 Heiser, J.E., METAFOR--A Verified Portable Translator Writing System, Ph.D. Thesis, Department of Computer Science, School of Engineering, University of California, June 1976.
15. 15 Husson, S., Microprogramming: Principles and Practices, Prentice Hall, Englewood Cliffs, N.J., 1970.
16. 16 Hewlett-Packard, A pocket guide to the 2100 computer, Palo Alto, California, 1966.
17. 17 Joyner, W.H., Jr., Carter, W.C., and Leeman, G.B., Jr., Automated proofs of microprogram correctness. Proc. 9th Ann. Workshop on Microprogramming, New Orleans, LA (Sept. 1976) pp. 9-14.
18. 18 Leeman, G.B., Jr., Some problems in certifying microprogramming. IEEE Trans. on Computers, C-24, 5, (May 1975) 543-553.
19. 19 Lehman, M.M., Microprogramming trend considered dangerous, Comm. ACM, 18, 6, (June 1975) 358-360.
20. 20 London, R.L. Correctness of two compilers for a LISP subset. Proc. ACM Conf. on Proving Assertions about Programs, New Mexico State University, Las Cruces, NM, Jan. 6-7, 1972, pp 121-127
21. 21 McKeeman, W.M., Peephole optimization. Comm. ACM, 8 7, (July 1965) 443-444.
22. 22 Milner, R., An algebraic definition of simulation between programs, Report No. CS-205, Stanford University, Feb. 1971.
23. 23 Patterson, D.A., The design of a system for the synthesis of correct microprograms, Proc. 8th Ann. Workshop on Microprogramming, Chicago, IL, September 21-23, 1975, pp 13-17.
24. 24 Patterson, D.A., STRUM: Structured microprogramming system for correct firmware. 1EEE Trans. on Computers, Special Issue on Microprogramming (October 1976) 974-985.
25. 25 Patterson, D.A., Verification of Microprograms, Ph.D. Thesis, University of California, UCLA-ENG-7707, January 1977.
26. 26 Patterson, D.A., Formal verification in an unverified environment: An experiment, Proc. of the 6th Texas Conf. on Computer Systems, Austin, TX, November, 1977. pp. 4A-13-4A-18.
27. 27 Patterson, D.A., An approach to firmware engineering. Proc. of the NCC, Anaheim, California, June 1978, p 643.
28. 28 Ragland, L.C., A Verified Program Verifier, Ph.D. Thesis, University of Texas, Austin, Texas, May 1973.
29. 29 Reigel, E.W. Faber, U., and Fisher, D.A., The interpreter--a microprogrammable building block system. Proc. of the SJCC, Anaheim, California, May 1972, pp. 705-723.
30. 30 Tucker, S.G., Microprogram control for System/360, IBM Syst. J. 6, 4, (April 1967) 222-241.
31. 31 Wilkes, M.V., The best way to design an automatic calculation machine, Manchester University Computer Inaugural Conference Proceedings, Manchester, England, 1951, p. 16.
32. 32 Wood, G., On packing of micro-operations into microinstruction words. Proc. 10th Ann. Workshop on Microprogramming, Niagara Falls, NY, September 19-22, 1978, pp. 51-55.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Mathematics of computing

  • Mathematical analysis

    • Mathematical optimization

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

      • Software defect analysis

        • Software testing and debugging

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Design and analysis of algorithms

    • Mathematical optimization

  • Semantics and reasoning

    • Program reasoning

      • Program verification