Abstract
It is argued that techniques for proving the correctness of hardware designs must use abstraction mechanisms for relating formal descriptions at different levels of detail. Four such abstraction mechanisms and their formalisation in higher order logic are discussed.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Camilleri, A.J., Gordon, M.J.C. and Melham, T.F., ‘Hardware Verification Using Higher Order Logic,’ to appear in: Proceedings of the IFIP International Conference: From H.D.L. Descriptions to Guaranteed Correct Circuit Designs, Grenoble, September 9–11, 1986.
Gordon, M.J.C., ‘HOL: A Machine Oriented Formulation of Higher Order Logic,’ Technical Report No. 68, Computer Laboratory, University of Cambridge, 1985.
Gordon, M.J.C., ‘HOL: A Proof Generating System for Higher Order Logic,’ in: VLSI Specification, Verification and Synthesis, G.M. Birtwistle and P.A. Subrahmanyam, eds., (this volume).
Gordon, M.J.C., ‘Why Higher Order Logic is a Good Formalism for Specifying and Verifying Hardware,’ in: Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh Conference on VLSI, G.J. Milne and P.A. Subrahmanyam, eds., North-Holland, Amsterdam, 1986.
Halbwachs, N., Lonchampt, A. and Pilaud, D., ‘Describing and Designing Circuits by means of a Synchronous Declarative Language,’ to appear in: Proceedings of the IFIP International Conference: From H.D.L. Descriptions to Guaranteed Correct Circuit Designs, Grenoble, September 9–11, 1986.
Hanna, F.K. and Daeche, N., ‘Specification and Verification using HigherOrder Logic: A Case Study,’ in: Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh Conference on VLSI, G.J. Milne and P.A. Subrahmanyam, eds., North-Holland, Amsterdam, 1986.
Hanna, F.K. and Daeche, N., ‘Specification and verification of digital systems using higher-order predicate logic,’ IEE Proceedings-E, VoL 133, Part E, No. 5, September 1986, pp. 242–254.
Herbert, J.M.J., Ph.D. Thesis, The University of Cambridge, to appear in 1987.
Hoare, C.A.R., ‘A Calculus of Total Correctness for Communicating Processes,’ Science of Computer Programming, Vol. 1, No. 1, 1981.
Leisenring, A., Mathematical Logic and Hilbert’s ∊-Symbol, Macdonald and Co. Ltd., London, 1969.
Winskel, G., ‘Lectures on models and logic of MOS circuits,’ Proceedings of the Marktoberdorf International Summer School on Logic Programming and Calculi of Discrete Design, July 1986.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1988 Kluwer Academic Publishers, Boston
About this chapter
Cite this chapter
Melham, T.F. (1988). Abstraction Mechanisms for Hardware Verification. In: Birtwistle, G., Subrahmanyam, P.A. (eds) VLSI Specification, Verification and Synthesis. The Kluwer International Series in Engineering and Computer Science, vol 35. Springer, Boston, MA. https://doi.org/10.1007/978-1-4613-2007-4_9
Download citation
DOI: https://doi.org/10.1007/978-1-4613-2007-4_9
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4612-9197-8
Online ISBN: 978-1-4613-2007-4
eBook Packages: Springer Book Archive