An experiment in high level language microprogramming and verification
- 1 October 1981
- journal article
- Published by Association for Computing Machinery (ACM) in Communications of the ACM
- Vol. 24 (10) , 699-709
- https://doi.org/10.1145/358769.358788
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.Keywords
This publication has 10 references indexed in Scilit:
- A 32b VLSI CPU chipPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1981
- An Overview of Firmware EngineeringComputer, 1978
- Observations of Fallibility in Applications of Modern Programming MethodologiesIEEE Transactions on Software Engineering, 1976
- Automated proofs of microprogram correctnessPublished by Association for Computing Machinery (ACM) ,1976
- The design of a system for the synthesis of correct microprogramsPublished by Association for Computing Machinery (ACM) ,1975
- On Proving Correctness of MicroprogramsIBM Journal of Research and Development, 1974
- Correctness of a compiler for a Lisp subsetPublished by Association for Computing Machinery (ACM) ,1972
- REDUCE 2Published by Association for Computing Machinery (ACM) ,1971
- Microprogram control for SYSTEM/360IBM Systems Journal, 1967
- Peephole optimizationCommunications of the ACM, 1965