Firmware quality assurance

ABSTRACT

The paper reviews problems, solutions, and trends in the area of firmware quality assurance. Firmware quality assurance is considered to be the certification of the fact that a firmware system meets its requirements with respect to functional correctness as well as performance, operational, and implementational properties. The emphasis of the paper is on formal correctness proofs, firmware testing, and the automatic synthesis of microcode and associated hardware structures. Firmware specifications, high-level microprogramming languages, and automated support tools are discussed as they relate to these areas. The impact of advances and trends in very large-scale integration (VLSI) on the techniques and tools for firmware quality assurance is reviewed. The observation is made that valuable results have been obtained in the areas of firmware correctness proofs and firmware testing. However, further improvements are needed to cope with the complexity of VLSI. An alternative that may overcome the limitations of these two approaches is automated synthesis of firmware and hardware and design for testability.

REFERENCES

• 1: Edward L. Robertson, Research note: microcode bit optimization is NP-hard, ACM SIGMICRO Newsletter, v.8 n.2, p.40-43, June 1977 [doi>10.1145/1217228.1217231]
• 2: Helmut K. Berg, Firmware testing and test data selection, Proceedings of the May 4-7, 1981, national computer conference, May 04-07, 1981, Chicago, Illinois [doi>10.1145/1500412.1500423]
• 3: David Landskov , Scott Davidson , Bruce Shriver , Patrick W. Mallett, Local Microcode Compaction Techniques, ACM Computing Surveys (CSUR), v.12 n.3, p.261-294, Sept. 1980 [doi>10.1145/356819.356822]
• 4: Alice C. Parker , Wayne T. Wilner, Microprogramming: the challenges of VLSI, Proceedings of the May 4-7, 1981, national computer conference, May 04-07, 1981, Chicago, Illinois [doi>10.1145/1500412.1500421]
• 5: Goodenough, J. B., S. L. Gerhart. "Toward a Theory of Test Data Selection" IEEE Transactions on Software Engineering, Vol. 1, No. 2, 1975, pp. 20--37.
• 6: Davidson, S., B. D. Shriver. "Firmware Engineering: An Extensive Update," in Firmware, Microprogramming and Restructurable Hardware. North-Holland Publ. Co., New York, 1980, pp. 1--40.
• 7: Richard A. De Millo , Richard J. Lipton , Alan J. Perlis, Social processes and proofs of theorems and programs, Communications of the ACM, v.22 n.5, p.271-280, May 1979 [doi>10.1145/359104.359106]
• 8: Husson, S. S. (panel chairman). "Microcode Verification---Summary of the Panel Discussion," in Firmware, Microprogramming and Restructurable Hardware, North-Holland Publ. Col., New York, 1980, pp. 105.
• 9: Carter, W. C., "Microcode Verification," Presentation in the Session on Microprogramming---The Challenge of the 1980's, 1981 National Computer Conference, Chicago, II.
• 10: Berg, H. K., W. E. Boebert, W. R. Franta, and T. G. Moher. Formal Methods of Program Verification and Specification, Prentice-Hall, Englewood Cliffs, N. J., 1982.
• 11: D. A. Patterson, Strum: Structured Microprogram Development System for Correct Firmware, IEEE Transactions on Computers, v.25 n.10, p.974-985, October 1976 [doi>10.1109/TC.1976.1674538]
• 12: Floyd, R. W. "Assigning Meaning to Programs," Proceedings of Symposia in Applied Mathematics, American Mathematical Society, Vol. 19, 1967, pp. 19--32.
• 13: Joyner, W. H., W. C. Carter, and G. B. Leeman. "Automated Proofs of Microprogram Correctness," SIGMICRO Newsletter, Vol. 7, No. 3, 1976, pp. 51--55.
• 14: Carter, W. C., H. C. Montgomery, R. J. Preiss, and H. J. Reinheimer. "Design of Serviceability Feature for the IBM System/360," IBM Journal, 1964, pp. 115--126.
• 15: Levendel, Y. H., and P. R. Menon. "Test Generation Algorithm for Non-procedural Hardware Description Languages", IEEE FTCS-11, 1981, pp. 200--105.
• 16: Su, S. Y. H., and C. L. Huang. "A Multi-Level Hardware Design Language LALSD II and its Translator," Proceedings of the 1981 International Symposium on CHDL's and Their Application, 1981.
• 17: Tsuchiya, M., and L. V. Ramamoorthy. "Design of a Multi-Level Micro-programmable Computer and a High-Level Microprogramming Language," University of Texas at Austin, Tech. Report 135, 1972.
• 18: F. J. Hill , B. Huey, SCIRTSS: A Search System for Sequential Circuit Test Sequences, IEEE Transactions on Computers, v.26 n.5, p.490-502, May 1977 [doi>10.1109/TC.1977.1674866]
• 19: Ciaramella, A. "Testing of Microprogrammed Units," IEEEFTCS-9, 1979, pp. 161--163.
• 20: Su, S. Y. M., and Yu-I Hsieh. "Testing Functional Faults in Digital Systems Described by Register Transfer Language," 1981 IEEE Test Conference, 1981, pp. 433--439.
• 21: Milner, R. "An Algebraic Definition of Simulation between Programs," Proceedings of the 2nd International Joint Conference on Artificial Intelligence, 1971, pp. 481--489.
• 22: J. A. Darringer , J. C. King, Applications of Symbolic Execution to Program Testing, Computer, v.11 n.4, p.51-60, April 1978 [doi>10.1109/C-M.1978.218139]
• 23: Crocker, S. D., L. Marcus, and D. van-Mierop. "The ISI Microcode Verification System," Firmware, Microprogramming and Restructurable Hardware, North-Holland Publ. Co., New York, 1980, pp. 89--103.
• 24: Dasgupta, S. "Some Implications of Programming Methodology for Microprogramming Language Design," Firmware, Microprogramming and Restructurable Hardware, North-Holland Publ. Co., New York, 1980, pp. 243--252.
• 25: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 26: R. H. Eckhouse, Jr., A high-level microprogramming language (MPL), Proceedings of the May 18-20, 1971, spring joint computer conference, May 18-20, 1971, Atlantic City, New Jersey [doi>10.1145/1478786.1478811]
• 27: Dewitt, D. J. "Extensibility---A New Approach for Designing Machine Independent Microprogramming Languages," SIGMICRO Newsletter, Vol. 7, No. 3, 1976, pp. 33--41.
• 28: Kamran Malik , Ted Lewis, Design objectives for high level microprogramming languages, ACM SIGMICRO Newsletter, v.9 n.4, p.154-160, Dec. 1978
• 29: Carter, W. C.; W. H. Joyner, and D. Brand. "Microprogram Verification Considered Necessary," Proceedings of the 1978 National Computer Conference, AFIPS Press, Arlington, Virginia, 1978, pp. 657--664.
• 30: Berg, H. K., and W. R. Franta. "Firmware Engineering: Critical Remarks and a Proposed Strategy," Firmware, Microprogramming and Restructurable Hardware, North-Holland Publ. Co., New York, 1980, pp. 41--64.
• 31: Richter, L. "High-Level Language Extensions for Micro-Code Generation and Verification," Firmware, Microprogramming and Restructurable Hardware, North-Holland Publ. Co., New York, 1980, pp. 233--242.
• 32: Davidson, S., and B. D. Shriver. "MARBLE: A High Level Machine Independent Language for Microprogramming," Firmware, Microprogramming and Restructurable Hardware, North-Holland Publ. Co., New York, 1980, pp. 253--266.
• 33: T. W. Williams , K. P. Parker, Design for Testability A Survey, IEEE Transactions on Computers, v.31 n.1, p.2-15, January 1982 [doi>10.1109/TC.1982.1675879]
• 34: Peter Marwedel, A retargetable microcode generation system for a high-level microprogramming language, ACM SIGMICRO Newsletter, v.12 n.4, p.115-123, Dec. 1981
• 35: Dono van-Mierop , Leo Marcus , Steve Crocker, Verification of the FTSC microprogram, ACM SIGMICRO Newsletter, v.9 n.4, p.118, Dec. 1978
• 36: G. Zimmermann, The MIMOLA design system a computer aided digital processor design method, Proceedings of the 16th Conference on Design automation, p.53-58, June 25-27, 1979, San Diego, CA, United States
• 37: S. M. Thatte , J. A. Abraham, Test Generation for Microprocessors, IEEE Transactions on Computers, v.29 n.6, p.429-441, June 1980 [doi>10.1109/TC.1980.1675602]
• 38: C. Robach , G. Saucier, Dynamic Testing of Control Units, IEEE Transactions on Computers, v.27 n.7, p.617-623, July 1978 [doi>10.1109/TC.1978.1675161]