This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Microprogramming Logic
May 1988 (vol. 14 no. 5)
pp. 559-574

A universal syntax-directed proof system is presented for the verification of horizontal computer architectures. The system is based on the axiomatic architecture description language AADL, which is sufficiently rich to allow the specification of target architectures while providing a concise model for clocked microarchitectures. For each description A epsilon AADL of a host, it is shown how to construct systematically a (Hoare-style) axiomatic definition of an A-dependent high-level microprogramming language based on S*. The axiomatization of A's microoperations together with a powerful proof-rule dealing with the inherent low-level parallelism of horizontal architectures allow a complete axiomatic treatment of the timing behavior and dynamic conflicts of microprograms written in S*(A).

[1] K. R. Apt, "Ten years of Hoare's-logic: A survey--Part one,"ACM Trans. Program. Lang. Syst., vol. 3, pp. 431-483, 1981.
[2] K. R. Apt, N. Francez, and W. P. de Roever, "A proof system for communicating sequential processes,"ACM Trans. Program Lang. Syst., vol. 2, no. 3, pp. 359-385, July 1980.
[3] J. de Bakker,Mathematical Theory of Program Correctness. London, England: Prentice-Hall, 1980.
[4] M. R. Barbacci, "Structural and behavioural description of digital systems," inNew Computer Architectures, J. Tiberghien, Ed. London: Academic, 1984.
[5] L. Bardis, "Ein Simulator-Generator für die S*-Familie," (in German), RWTH Aachen, Tech. Rep., 1984.
[6] H. K. Berg, "Correctness of firmware--An overview," inProc. Seminarüber Firmware Engineering(Informatik-Fachberichte 31). Berlin: Springer-Verlag, 1980, pp. 173-224.
[7] H. K. Berg, R. Rao, and B. D. Shriver, "Firmware quality assurance," inProc. Nat. Comput. Conf., 1982, pp. 4-10.
[8] D. Brand and W. H. Joyner, "Verification of protocols using symbolic execution,"ACM Comput. Networks, vol. 2, pp. 351-360, 1978.
[9] D. Brand and W. H. Joyner, "Verification of HDLC,"IEEE Trans. Commun., vol. Com- 30, no. 5, pp. 1136-1142, 1982.
[10] J. de Bakker,Mathematical Theory of Program Correctness. London, England: Prentice-Hall, 1980.
[11] W. C. Carter, W. H. Joyner, and D. Brand, "Microprogram verification considered necessary," inProc. Nat. Comput. Conf., vol. 47, 1978, pp. 657-664.
[12] Carter, W.J., W.H. Joyner, and D. Brand, "Symbolic Simulation for Correct Machine Design,"ACM IEEE 16th Design Automation Conf., June 1979, pp. 280-286.
[13] C. L. Chang and R. C. T. Lee,Symbolic Logic and Mechanical Theorem Proving. New York: Academic, 1973.
[14] S. A. Cook, "Soundness and completeness of an axiom system for program verification,"SIAM J. Comput., vol. 7, pp. 70-90, 1978.
[15] S. D. Crocker, "State deltas: A formalism for representing segments of computation," Univ. Southern California, Tech. Rep. ISI/RR-77- 61, 1977.
[16] S. D. Crocker, L. Marcus, and D. van Mierop, "The ISI microcode verification system," inFirmware, Microprogramming and Restructurable Hardware, G. Chroust and J. R. Mühlbacher, Eds. Amsterdam, The Netherlands: North-Holland, 1980, pp. 89-103.
[17] W. Damm, "Automatic generation of simulation tools: A case study in the design of a retargetable firmware development system," inAdvances in Microprocessing and Microprogramming, B. Myhrhaug and D. R. Wilson, Eds. Amsterdam, The Netherlands: North-Holland, 1984, pp. 165-176.
[18] W. Damm, "An axiomatization of low-level parallelism in microarchitectures," inProc. MICRO-17, New Orleans, LA, Washington, DC: IEEE Computer Society Press, 1984, pp. 314-323.
[19] W. Damm, "Entwurf und Verifikation mikroprogrammierter Rechnerarchitekturen" (in German), inInformatik Fachberichte. W. Brauer, Ed. Berlin: Springer-Verlag, 1987.
[20] W. Damm, G. Doehmen, K. Merkel, and M. Sichelschmidt, "The AADL/S*approach to firmware design verification,"IEEE Software, vol. 3, no. 4, pp. 27-37, 1986.
[21] W. Damm and G. Doehmen, "Verification of microprogrammed computer architectures in the S*-system: A case study," inProc. MICRO- 18. Washington, DC: IEEE Computer Society Press, 1985, pp. 61- 73.
[22] S. Dasgupta, "Towards a microprogramming language scheme," inProc.MICRO-11, 1978, pp. 144-153.
[23] S. Dasgupta, "Some implications of programming methodology for microprogramming language design," inFirmware, Microprogramming and Restructurable Hardware, G. Chroust and J. R. Mühlbacher, Eds. Amsterdam, The Netherlands: North-Holland, 1980, pp. 243-252.
[24] S. Dasgupta, "Some aspects of high-level microprogramming,"Comput. Surveys, vol. 12, no. 3, pp. 195-323, 1980.
[25] S. Dasgupta, "Computer design and description languages,"Advances in Comput., vol. 21, pp. 91-154, 1982.
[26] S. Dasgupta, personal communication.
[27] S. Dasgupta and A. Wagner, "The use of Hoare logic in the verification of horizontal microprograms," inProc. MICRO-16, 1983.
[28] S. Dasgupta,The Design&Description of Computer Architectures, John Wiley&Sons, New York, 1984.
[29] S. Dasgupta, "Principles of firmware verification," inHandbook of Microprogramming and Firmware Engineering, S. Habib and S. Dasgupta, Eds. New York: van Nostrand, 1984.
[30] S. Dasgupta, "A model of clocked micro-architectures for firmware-engineering and design automation applications," inProc. MICRO-17, New Orleans, LA, 1984.
[31] S. Davidson and B. D. Shriver, "Firmware engineering: An extensive update," inFirmware, Microprogramming and Restructurable Hardware, G. Chroust and J. R. Mühlbacher, Eds. Amsterdam, The Netherlands: North-Holland, 1980, pp. 1-37.
[32] P. Dembinski and S. Budkowski, "Verification, design and description oriented microprogramming language," inProc. Conf. Large Scale Integration, H. W. Lawson, H. Berndt, and G. Hermanson, Eds. Amsterdam, The Netherlands: North-Holland, 1978, pp. 230- 240.
[33] P. Dembinski, "Design and verification oriented microprogram transformations," inProc. IFIP-Conf. Programming Languages and System Design, J. Bormann, ed. Amsterdam, The Netherlands: North-Holland, 1983, pp. 141-155.
[34] E. W. Dijkstra,A Discipline of Programming. Englewood Cliffs, NJ: Prentice-Hall, 1976.
[35] R. W. Floyd, "Assigning Meanings to programs," inProc. Symp. Applied Mathematics, J. T. Schwartz, Ed., Amer. Math. Soc., 1967, pp. 19-32.
[36] M. Ganapathi and C. N. Fisher "A review of automatic code-generation techniques," Univ. Madison, Tech. Rep. 407, 1981.
[37] S. L. Gerhard, D. R. Musser, D. J. Thompson, and D. A. Baker, R. L. Bates, R. W. Erickson, R. L. London, D. G. Taylor, D. S. Wile, "An overview of AFFIRM: A specification and verification system," inInform. Processing '80, S. H. Lavingron, Ed. Amsterdam, The Netherlands: North-Holland, 1980, pp. 343-347.
[38] D. I. Good, R. M. Cohen, C. G. Hoch, L. W. Hunter, and D. F. Hore, "Gypsy, 2.0 programming system 6.0 user's manual," Certifiable Minicomputer Project, Univ. Texas at Austin, 1979.
[39] M. Gordon, "LCF-LSM," Univ. Cambridge, Tech. Rep. 41, 1983.
[40] M. Gordon, "Proving a computer correct," Univ. Cambridge, Tech. Rep. 42, 1983.
[41] D. Gries,The Science of Programming. New York: Springer-Verlag, 1981.
[42] C. A. R. Hoare, "An axiomatic basis for computer programming,"Commun. ACM, vol. 12, no. 10, pp. 576-583, 1969.
[43] S. Igarashi, R. L. London, and D. C. Luckham, "Automatic program verification I: A logical basis and its implementation,"Acta Inform., vol. 4, pp. 145-182, 1975.
[44] W. H. Joyner and A. Birman, "Proving simulations between programs," IBM Res. Rep. RC 5091, 1974.
[45] W. H. Joyner, W. C. Carter, and D. Brand, "Using machine descriptions in program verification," inInformation Technology, J. Moneta, Ed. Amsterdam, The Netherlands: North-Holland, 1978.
[46] W. H. Joyner, W. C. Carter, and G. B. Leeman, "Automated proofs of microprogram correctness," inProc. Micro-9, 1976, pp. 51-55.
[47] A. B. Klassen, "S*(QM-1): An experimental evaluation of the high-level microprogramming language scheme S*using the nanodata QM- 1," Dep. Comput. Sci., Univ. Alberta, Tech. Rep. TR 81-10, 1981.
[48] D. C. Luckham, "Program verification and verification oriented programming," inProc. Information Processing 77, AFIPS no. 4, 1977, pp. 783-793.
[49] P. Marwedel, "Hardware allocation for horizontal microinstructions in the MIMOLA software system," Institut für Informatik und Praktische Mathematik, Universität Kiel, Tech. Rep. 5/80, 1980.
[50] P. Marwedel, "A retargetable microcode generation system for a high-level microprogramming language," inProc. Micro-14, 1981, pp. 115- 123.
[51] P. Marwedel, "A retargetable compiler for a high-level microprogramming languages," inProc. MICRO-17. Washington, DC: IEEE Computer Society Press, 1984, pp. 267-274.
[52] K. Merkel, "Formale Definition einer Familie von high-level Mikroprogrammiersprachen," RWTH Aachen, Tech. Rep., 1983.
[53] R. Miiner, "An algebraic definition of simulation between programs," inProc. 2nd Conf. Artificial Intelligence (IJCAI-2), London, 1971, pp. 481-489.
[54] R. A. Mueller,Automated Microprogram Synthesis. Ann Arbor, MI: UMI Research Press, 1984.
[55] S. Owicki and D. Gries, "Verifying properties of parallel programs: An axiomatic approach,"Commun. ACM, vol. 19, pp. 279-285, May 1976.
[56] D. Patterson, "STRUM: Structured microprogram development system for correct firmware,"IEEE Trans. Comput., vol. C-25, no. 10, pp. 974-984, 1976.
[57] D. Patterson, "Verification of microprograms," UCLA, Rep. ENG-7707, 1977.
[58] D. Patterson, "An approach to firmware engineering," inProc. Nat. Comput. Conf., vol. 47, 1978, pp. 643-647.
[59] D. Patterson, "An experiment in high-level language microprogramming and verification,"Commun. ACM, vol. 24, no. 10, pp. 699-709, 1981.
[60] P. Raulefs and J. Seikmann, "Programmverifikation," Univ. Kaiserslautern, Tech. Rep., 1980.
[61] M. M. Richter,Logikkalküle. Berlin: Teubner-Verlag, 1978.
[62] J. R. Shoenfield,Mathematical Logic. Reading, MA: Addison-Wesley, 1967.
[63] D. H. Thompson and R. W. Erickson,AFFIRM Reference ManualUSC Inform. Sci. Inst., Marina del Ray, CA, 1981.
[64] G. Zimmerman, "MDS--The Mimola design method,"J. DXX Syst., vol. 4, no. 3, pp. 337-369, 1980.
[65] L. Marcus, S. D. Crocker, and J. R. Landauer, "SDVS: A system for verifying microcode correctness," inProc. MICRO-17. Washington, DC: IEEE Computer Society Press, 1984, pp. 246-255.
[66] R. Beccard, "Automatische und vollständige Generierung von Korrektheitsbeweisen für Mikroprogramme," (in German), RWTH Aachen, Tech. Rep., May 1986.
[67] D. Landskov, S. Davidson, B. D. Shriver, and P. W. Mallett, "Local microcode compaction techniques,"ACM Comput. Surveys, vol. 12, no. 3, pp. 261-294, Sept. 1980.
[68] R. Beccard, W. Datum, G. Doehmen, and M. Sichelschmidt, "Two techniques for automating firmware design verification," inProc. CHDL 87. Amsterdam, The Netherlands: North-Holland, 1987, pp. 249-265.
[69] Microprogramming Handbook, Microdata Corp., Irvine, CA, 1972.
[70] How to Use the NOVA Computers, Data General Corp., Southboro, MA, 1972.
[71] W. Damm and G. Doehmen, "An axiomatic approach to the specification of distributed computer architectures," inProc. PARLE, J. de Bakker, A. Nijman, and P. Treleavan, Eds. Berlin: Springer-Verlag, 1987, pp. 103-120.

Index Terms:
microprogramming logic; syntax-directed proof system; horizontal computer architectures; architecture description language; AADL; specification; clocked microarchitectures; axiomatic definition; microoperations; low-level parallelism; timing behavior; dynamic conflicts; computer architecture; formal logic; microprogramming; specification languages; theorem proving
Citation:
W. Damm, "A Microprogramming Logic," IEEE Transactions on Software Engineering, vol. 14, no. 5, pp. 559-574, May 1988, doi:10.1109/32.6134
Usage of this product signifies your acceptance of the Terms of Use.