Abstract
This paper describes the formal verification of two memory management units using the HOL theorem prover. The verification effort demonstrates the use of hierarchical decomposition and abstract theories. Both devices authorize memory requests and translate virtual addresses to real addresses. The first unit was designed and verified to the gate level. The second memory management unit is implemented with an abstract representation and provides some operating system support. Memory requests are validated based on a memory resident segment table. These units are being used as a basis for the verification of a composed chip set to form a trusted computing base.
This work was sponsored under Boeing Contract NAS1-18586, Task Assignment No. 3, with NASA-Langley Research Center
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
V. P. Nelson, “Fault-Tolerant Computing: Fundamental Concepts,” Computer, July 1990.
H. G. Barrow, “VERIFY: A Program for Proving Correctness of Digital Hardware Designs,” Artificial Intelligence, vol. 24, 1984.
J. J. Joyce, “Formal Specification and Verification of Microprocessor Systems,” Microprocessing and Microprogramming, North-Holland, vol. 24, 1988.
G. Milne and P. Subrahmanyam, Formal Aspect of VLSI Design. Publishers B.V., 1986.
D. Weise, “Functional Verification of MOS Circuits,” 24th ACM/IEEE Design Automation Conference, 1987.
W. A. Hunt, “Microprocessor Design Verification,” Journal of Automated Reasoning, vol. 5, 1989.
W. R. Bevier, W. A. Hunt, and W. D. Young, “Toward Verified Execution Environments,” IEEE Symposium on Security and Privacy, 1987.
W. R. Bevier, “Kit and the Short Stack,” Journal of Automated Reasoning, vol. 5, 1989.
P. J. Windley, “A Hierarchical Methodology for Verifying Microprogrammed Microprocessors,” IEEE Symposium on Research in Security and Privacy, 1990.
J. Pan and K. N. Levitt, “A Formal Specification of the IEEE Floating-Point Standard with Application to the Verification of Floating-Point Coprocessors and Numerical Arithmetic,” Proceedings of 24th Asilomar Conference on Signals, Systems and Computers, 1990.
P. J. Windley, The Formal Verification of Generic Interpreters. PhD thesis, University of California, Davis, 1990.
E. T. Schubert, “Verification of Memory Management Units using HOL,” technical report CSE-90-27, University of California, Davis, August 1990.
P. G. Neumann, “On Hierarchical Design of Computer Systems for Critical Applications,” IEEE Transaction on Software Engineering, vol. SE-12, No. 9, September 1986.
J. D. Guttman and H. Ko, “Verifying A Hardware Security Architecture,” IEEE Symposium on Research in Security and Privacy, 1990.
A. Cohn, “A Proof of Correctness of the VIPER Microprocessor: the Second Level,” in VLSI Specification, Verification, and Synthesis, (G. Birtwhistle and P. Subrahmanyam, eds.), Springer-Verlag, 1989.
W. A. Hunt, “A Verified Microprocessor,” technical report 47, The University of Texas at Austin, Dec. 1985.
J. J. Joyce, Multi-Level Verification of Microprocessor-Based Systems. PhD thesis, Cambridge University, December 1989.
W. J. Cullyer, “Implementing Safety Critical Systems: The VIPER Microprocessor,” in VLSI Specification, Verification, and Synthesis, (G. Birtwhistle and P. Subrahmanyam, eds.), Kluwer Academic Press, 1988.
J. J. Joyce, “Totally Verified Systems: Linking Verified Software to Verified Hardware,” Hardware Specification, Verification and Synthesis: Mathematical Aspects, July 1989.
W. R. Bevier, “A Verified Operating System Kernel,” technical report 11, Computational Logic, Inc., October 1989.
M. Gordon, “HOL: A Proof Generating System for Higher-Order Logic,” in VLSI Specification, Verification, and Synthesis, (G. Birtwhistle and P. Subrahmanyam, eds.), Kluwer Academic Press, 1988.
W. Boebert, “The LOCK Demonstration,” 11 th National Computer Security Conference, 1988.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1992 Springer-Verlag/Wien
About this paper
Cite this paper
Schubert, E.T., Levitt, K.N. (1992). Verification of Memory Management Units. In: Meyer, J.F., Schlichting, R.D. (eds) Dependable Computing for Critical Applications 2. Dependable Computing and Fault-Tolerant Systems, vol 6. Springer, Vienna. https://doi.org/10.1007/978-3-7091-9198-9_13
Download citation
DOI: https://doi.org/10.1007/978-3-7091-9198-9_13
Publisher Name: Springer, Vienna
Print ISBN: 978-3-7091-9200-9
Online ISBN: 978-3-7091-9198-9
eBook Packages: Springer Book Archive