Abstract
Microcode is used to facilitate new technologies in Intel CPU designs. A critical requirement is that new designs be backwardly compatible with legacy code when new functionalities are disabled. Several features distinguish microcode from other software systems, such as: interaction with the external environment, sensitivity to exceptions, and the complexity of instructions. This work describes the ideas behind MICROFORMAL,, a technology for fully automated formal verification of functional backward compatibility of microcode.
This research was supported in part by SRC grant 2004-TJ-1256, NSF grants CCF-0456163, CCR-9988322, CCR-0124077, CCR-0311326, IIS-9908435, IIS-9978135, EIA-0086264, ANI-0216467, BSF grant 9800096, and by Texas ATP grant 003604-0058-2003.
Chapter PDF
Similar content being viewed by others
References
Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998)
Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL 2002, pp. 1–3 (2002)
Currie, D.W., Hu, A.J., Rajan, S., Fujita, M.: Automatic formal verification of DSP software. In: DAC 2000, pp. 130–135 (2000)
Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: DAC 2003, pp. 368–371 (2003)
Cyrluk, D.: Microprocessor Verification in PVS: A Methodology and Simple Example. Technical Report SRI-CSL-93-12, Menlo Park, CA (1993)
Feng, X., Hu, A.J.: Automatic formal verification for scheduled VLIW code. In: ACM SIGPLAN Joint Conference: Languages, Compilers, and Tools for Embedded Systems, and Software and Compilers for Embedded Systems, pp. 85–92 (2002)
Huang, S.Y., Cheng, K.T.: Formal Equivalence Checking and Design Debugging. Kluwer, Dordrecht (1998)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)
Harel, D., Pnueli, A.: On the development of reactive systems. In: Logics and Models of Concurrent Systems. NATO ASI Series, vol. F-13, pp. 477–498 (1985)
Hamaguchi, K., Urushihara, H., Kashiwabara, T.: Symbolic checking of signal-transition consistency for verifying high-level designs. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 455–469. Springer, Heidelberg (2000)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)
Necula, G.: Translation validation of an optimizing compiler. In: PLDI 2000, pp. 83–94 (2000)
Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, p. 151. Springer, Heidelberg (1998)
Sawada, J., Hunt, W.A.: Verification of FM9801: An out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability. J. on Formal Methods in System Design 20(2), 187–222 (2002)
Srivas, M., Miller, S.: Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods. J. on Formal Methods in System Design 8, 153–188 (1996)
Stallings, W.: Computer Organization and Architecture, 6th edn. Prentice-Hall, Englewood Cliffs (2002)
Zuck, L., Pnueli, A., Fang, Y., Goldberg, B.: Voc: A translation validator for optimizing compilers. J. of Universal Computer Science 9(2) (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Arons, T. et al. (2005). Formal Verification of Backward Compatibility of Microcode. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_20
Download citation
DOI: https://doi.org/10.1007/11513988_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.