
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
W. Damm, "A Microprogramming Logic," IEEE Transactions on Software Engineering, vol. 14, no. 5, pp. 559574, May, 1988.  
BibTex  x  
@article{ 10.1109/32.6134, author = {W. Damm}, title = {A Microprogramming Logic}, journal ={IEEE Transactions on Software Engineering}, volume = {14}, number = {5}, issn = {00985589}, year = {1988}, pages = {559574}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.6134}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  A Microprogramming Logic IS  5 SN  00985589 SP559 EP574 EPD  559574 A1  W. Damm, PY  1988 KW  microprogramming logic; syntaxdirected proof system; horizontal computer architectures; architecture description language; AADL; specification; clocked microarchitectures; axiomatic definition; microoperations; lowlevel parallelism; timing behavior; dynamic conflicts; computer architecture; formal logic; microprogramming; specification languages; theorem proving VL  14 JA  IEEE Transactions on Software Engineering ER   
A universal syntaxdirected 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 (Hoarestyle) axiomatic definition of an Adependent highlevel microprogramming language based on S*. The axiomatization of A's microoperations together with a powerful proofrule dealing with the inherent lowlevel 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'slogic: A surveyPart one,"ACM Trans. Program. Lang. Syst., vol. 3, pp. 431483, 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. 359385, July 1980.
[3] J. de Bakker,Mathematical Theory of Program Correctness. London, England: PrenticeHall, 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 SimulatorGenerator für die S*Familie," (in German), RWTH Aachen, Tech. Rep., 1984.
[6] H. K. Berg, "Correctness of firmwareAn overview," inProc. Seminarüber Firmware Engineering(InformatikFachberichte 31). Berlin: SpringerVerlag, 1980, pp. 173224.
[7] H. K. Berg, R. Rao, and B. D. Shriver, "Firmware quality assurance," inProc. Nat. Comput. Conf., 1982, pp. 410.
[8] D. Brand and W. H. Joyner, "Verification of protocols using symbolic execution,"ACM Comput. Networks, vol. 2, pp. 351360, 1978.
[9] D. Brand and W. H. Joyner, "Verification of HDLC,"IEEE Trans. Commun., vol. Com 30, no. 5, pp. 11361142, 1982.
[10] J. de Bakker,Mathematical Theory of Program Correctness. London, England: PrenticeHall, 1980.
[11] W. C. Carter, W. H. Joyner, and D. Brand, "Microprogram verification considered necessary," inProc. Nat. Comput. Conf., vol. 47, 1978, pp. 657664.
[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. 280286.
[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. 7090, 1978.
[15] S. D. Crocker, "State deltas: A formalism for representing segments of computation," Univ. Southern California, Tech. Rep. ISI/RR77 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: NorthHolland, 1980, pp. 89103.
[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: NorthHolland, 1984, pp. 165176.
[18] W. Damm, "An axiomatization of lowlevel parallelism in microarchitectures," inProc. MICRO17, New Orleans, LA, Washington, DC: IEEE Computer Society Press, 1984, pp. 314323.
[19] W. Damm, "Entwurf und Verifikation mikroprogrammierter Rechnerarchitekturen" (in German), inInformatik Fachberichte. W. Brauer, Ed. Berlin: SpringerVerlag, 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. 2737, 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.MICRO11, 1978, pp. 144153.
[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: NorthHolland, 1980, pp. 243252.
[24] S. Dasgupta, "Some aspects of highlevel microprogramming,"Comput. Surveys, vol. 12, no. 3, pp. 195323, 1980.
[25] S. Dasgupta, "Computer design and description languages,"Advances in Comput., vol. 21, pp. 91154, 1982.
[26] S. Dasgupta, personal communication.
[27] S. Dasgupta and A. Wagner, "The use of Hoare logic in the verification of horizontal microprograms," inProc. MICRO16, 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 microarchitectures for firmwareengineering and design automation applications," inProc. MICRO17, 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: NorthHolland, 1980, pp. 137.
[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: NorthHolland, 1978, pp. 230 240.
[33] P. Dembinski, "Design and verification oriented microprogram transformations," inProc. IFIPConf. Programming Languages and System Design, J. Bormann, ed. Amsterdam, The Netherlands: NorthHolland, 1983, pp. 141155.
[34] E. W. Dijkstra,A Discipline of Programming. Englewood Cliffs, NJ: PrenticeHall, 1976.
[35] R. W. Floyd, "Assigning Meanings to programs," inProc. Symp. Applied Mathematics, J. T. Schwartz, Ed., Amer. Math. Soc., 1967, pp. 1932.
[36] M. Ganapathi and C. N. Fisher "A review of automatic codegeneration 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: NorthHolland, 1980, pp. 343347.
[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, "LCFLSM," 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: SpringerVerlag, 1981.
[42] C. A. R. Hoare, "An axiomatic basis for computer programming,"Commun. ACM, vol. 12, no. 10, pp. 576583, 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. 145182, 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: NorthHolland, 1978.
[46] W. H. Joyner, W. C. Carter, and G. B. Leeman, "Automated proofs of microprogram correctness," inProc. Micro9, 1976, pp. 5155.
[47] A. B. Klassen, "S*(QM1): An experimental evaluation of the highlevel microprogramming language scheme S*using the nanodata QM 1," Dep. Comput. Sci., Univ. Alberta, Tech. Rep. TR 8110, 1981.
[48] D. C. Luckham, "Program verification and verification oriented programming," inProc. Information Processing 77, AFIPS no. 4, 1977, pp. 783793.
[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 highlevel microprogramming language," inProc. Micro14, 1981, pp. 115 123.
[51] P. Marwedel, "A retargetable compiler for a highlevel microprogramming languages," inProc. MICRO17. Washington, DC: IEEE Computer Society Press, 1984, pp. 267274.
[52] K. Merkel, "Formale Definition einer Familie von highlevel Mikroprogrammiersprachen," RWTH Aachen, Tech. Rep., 1983.
[53] R. Miiner, "An algebraic definition of simulation between programs," inProc. 2nd Conf. Artificial Intelligence (IJCAI2), London, 1971, pp. 481489.
[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. 279285, May 1976.
[56] D. Patterson, "STRUM: Structured microprogram development system for correct firmware,"IEEE Trans. Comput., vol. C25, no. 10, pp. 974984, 1976.
[57] D. Patterson, "Verification of microprograms," UCLA, Rep. ENG7707, 1977.
[58] D. Patterson, "An approach to firmware engineering," inProc. Nat. Comput. Conf., vol. 47, 1978, pp. 643647.
[59] D. Patterson, "An experiment in highlevel language microprogramming and verification,"Commun. ACM, vol. 24, no. 10, pp. 699709, 1981.
[60] P. Raulefs and J. Seikmann, "Programmverifikation," Univ. Kaiserslautern, Tech. Rep., 1980.
[61] M. M. Richter,Logikkalküle. Berlin: TeubnerVerlag, 1978.
[62] J. R. Shoenfield,Mathematical Logic. Reading, MA: AddisonWesley, 1967.
[63] D. H. Thompson and R. W. Erickson,AFFIRM Reference ManualUSC Inform. Sci. Inst., Marina del Ray, CA, 1981.
[64] G. Zimmerman, "MDSThe Mimola design method,"J. DXX Syst., vol. 4, no. 3, pp. 337369, 1980.
[65] L. Marcus, S. D. Crocker, and J. R. Landauer, "SDVS: A system for verifying microcode correctness," inProc. MICRO17. Washington, DC: IEEE Computer Society Press, 1984, pp. 246255.
[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. 261294, 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: NorthHolland, 1987, pp. 249265.
[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: SpringerVerlag, 1987, pp. 103120.