W. Damm
ABSTRACT
This paper presents a hierarchical firmware design method. It allows to structure the design of a microprogrammed (level of a) computer architecture into independently verifiable modules. To specify the behaviour of the system we use the axiomatic architecture description language AADL. We illustrate the design and specification style using an emulation example.
- 1.Amdahl,G.M., Blaauw,G.A., and Brooks.F.P. Architecture of the IBM-System-360 IBM J. of Research and Development, Vol. 8, 1964, 78-101Google Scholar
Digital Library
- 2.Balzert,H. Die EntwickZung von Software-Systemen BI-Wissenschaftsverlag, ReiheInformatiik 34, 1982Google Scholar
- 3.Banerji,D.K. and Raymond,J. EZements Of Microprogramming Prentice-Hall, 1982Google Scholar
- 4.Beccard,R. Implementierung sines Verificationsbedingungsgenemtors fUr die S*-Familie haherer Mikroprogramniersprachen, in preparationGoogle Scholar
- 5.Bell,C.G., and Newell,A. Computer Structures: Readings and Examples MC Graw:Hdll.lN.Y.,1971 Google ScholarDigital Library
- 6.Berg,H.K., and Franta,W.R. Firmware Engineering: Critica Remarks anda tioposed Strategy in: Firmware, Microprogramming and Restructurahle Hardware, edts. G. Chroust and J. Miihlbacher, North-Holland, 1980, 41-63Google Scholar
- 7.Damm, W. Automatic Generation of Simulation Tools: A Case Study in the Design of a Retargetable Firmre Development System in: Advances in Microprocessing and Microprogramming, edts.: B. Myrhaug and D. R. Wilson, North-Holland, 1984'., 165-176Google Scholar
- 8.Damm, W. An Axiomatization of Lok Level Parallelism in Micro architectures Proc. MICRO-17, IEEE Computer Society Press, 1984, 314-323 Google ScholarDigital Library
- 9.Darnm, W. A Microprogramming Logic Schriftenzur Informatikund Angew and ten Mathematiko. 98, RNTH Aachen, 1984Google Scholar
- 10.Damm, W. Enntwuxf und Verification Microprogrammierter Rechnerarchitecturen WrH Aachen,1985Google Scholar
- 11.Damm, W ., Langmaack, H., Penner, V., and Richter, M. Ein System zur incrementellen Entwicklungund Verificationen von Microprogrammen and Rechnerarchitekturen RWTH Aachen and University Kiel, 1984Google Scholar
- 12.Damm, W. and D Bhmen, G. Verification of Microprogrammed Computer Architectures in the S*-System: A case study Proc. this conference, 1985Google Scholar
- 13.Damm, W. Specification and Validation of Computer Architectures in the S*-System 1985, to appearGoogle Scholar
- 14.Dasgupta, S. Towards a Microprogramming Language Schema Proc. Micro-11, 1978, 144-153 Google ScholarDigital Library
- 15.Dasgupta, S. The Design and Description of computer Architectures J. WiIey & Sons, 1984 Google ScholarDigital Library
- 16.Dasgupta, S., Heinanen, J. On the Axiomatic Specification of Computer Architectures Proc. 7th Int. Conf. on Hardware Description Languages, Tokyo, 1985Google Scholar
- 17.Davidson, S., and Shriver, B.D. Specifying Target Resources ina Machine Independent Higher Level Language National Comp. Conference, 1981, 81-85Google Scholar
- 18.Dohmen, G. Verification sines Emulators: Eine Fallstudie zur Verification microprogrammierter Rechnerarchitekturen Diplomarbeit, RWTH Aachen, 1985Google Scholar
- 19.Fuller, S.H., Shannon, P., Lamb, D., and Burr, N. E. Evaluation of Computer Architectures via Test- Programs Proc. AFIP Nat. Comp. Conf. Vol. 46. AFLP-Press, 1977, 14/-1960Google Scholar
- 20.Giloi, W. K., Behr, P., and Gueth, R. FIT-A System for Firmware Specification, Implementation, and Validation in: Firmware, Microprogramming and Restructurable Hardware, edts.: G. Chroustand J. Muhlbacher, North-Holland, 1980, 217-232Google Scholar
- 21.Giloi, W. K., Gueth, R., and Shriver, B. D. Firmware Engineering: Methods and Tools for Firmware Specification and Design Nat. Comp. Conf., 1981, 49-55Google Scholar
- 22.How to use NOVA-computers Southhorough, Massachusetts, DataGeneralCorp., 1972,Google Scholar
- 23.Levy, B. Microcode Verification using SDVS-The Methodand a Case Study Proc.MICRO-17,IEEE Press, 1984, 234-245 Google ScholarDigital Library
- 24.Levitt, K., Robinson, L. Proof Techniques for Hierarchically Structured Programs in: current Trends in Programming Methodology II, edt. R. Yeh, Englewood Cliffs, PrenticeHall, NewJersey, 1977Google Scholar
- 25.Levitt, K. N., Robinson, L., and Silverberg, B. A. The HDMH and book SRI-International, 1979Google Scholar
- 26.Microprogramming Handbook 2nd edition, Microdata Carp, Irvine, Calif. 1972Google Scholar
- 27.Robinson, L., Levitt, K. N, Proof Techniques for Hierarchically Structured Programs Comm. ACM, vol. 20, 1977, 271-283 Google ScholarDigital Library
- 28.Sichelschmidt, I. Formater Enturf von Bitiles Microprocessoren in AADL in preparationGoogle Scholar
Index Terms
- Design and specification of microprogrammed computer architectures
Recommendations
Design and specification of microprogrammed computer architectures
This paper presents a hierarchical firmware design method. It allows to structure the design of a microprogrammed (level of a) computer architecture into independently verifiable modules. To specify the behaviour of the system we use the axiomatic ...
Design and Implementation of a Tool for Specifying Specification in SOFL
Revised Selected Papers of the Second International Workshop on Structured Object-Oriented Formal Language and Method - Volume 7787Structure Object-oriented Formal Language SOFL is not just a formal language for writing formal specification. It is also an approach and a methodology. SOFL provides a three-step approach for modelling a software system using formal specification. ...
Formal Specification and Design Time Testing
It is shown how design time testing can be used in conjunction with formal specification. Emphasis is placed on the benefits of using an executable specification language OBJ, of having a design controlled by requirements specification, and of adherence ...
Comments