Abstract
The stack is an ubiquitous component in both software and hardware. It is used as an ADT in data structures, while it serves as a component from floating point units to instruction execution units. In this paper, we explore the specification and verification of a simple bounded stack at differing levels of abstraction. We use HOL theorem proving at higher abstraction levels, while using VOSS symbolic trajectory evaluation at the switch-level. This case study provided a simple context to study various issues involved in combining theorem proving and symbolic simulation. Symbolic trajectory evaluation gives us access to accurate circuit models as well as the advantage of automating most of the proof effort. Theorem-proving gives us the expressive power for specification, than would generally be possible in a model checker approach. Further, we add executability to this combination to evaluate HOL theorem prover specifications. Executing HOL specifications helps detect errors before embarking on tedious proofs.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Albert Camilleri, “Executing behavioural definitions in higher order logic”, Technical Report 140, University of Cambridge, Computer Laboratory, February 1988.
Juanito Camilleri, “Symbolic compilation and execution of programs by proof: a case study in HOL”, Technical Report 240, University of Cambridge, Computer Laboratory, December 1991.
Paul Curzon, “Of what use is a verified compiler specification?”, Technical Report 274, University of Cambridge, Computer Laboratory, November 1992.
Goguen, Joseph A., “OBJ as a Theorem Prover with Applications to Hardware Verification”, in: Birtwistle, G. and Subrahmanyam, P., eds., Current Trends in Hardware Verification and Automated Theorem Proving, Springer Verlag, 1989, pp 218–267.
Gordon, M.J.C, “Why Higher Order Logic is a Good Formalism for Specifying and Verifying Hardware”, in: Milne, G. and Subrahmanyam, P., eds., Formal Aspects o f VLSI Design, Proceedings of the 1985 Edinburgh Conference on VLSI, North Holland, 1986, pp 153–177.
Joyce, Jeffrey and Seger, C-J, “Linking BDD-Based Symbolic Evaluation to Interactive Theorem-Proving”, To Appear in Proceedings of the 30th ACM-IEEE Design Automation Conference, IEEE, 1993
Joyce, Jeffrey and Seger, C-J, “The HOL Voss System: Model-Checking in a General Purpose Theorem Prover”, To Appear in Proceedings of the International Workshop on Higher Order Logic Theorem Proving and its Applications, Vancouver BC, Canada, 1993, Springer Verlag.
Melham, Tom, “Automating Recursive Type Definitions in HOL”, Current Trends in Hardware Verification and Automated Theorem Proving, Springer Verlag, 1989
Rajan, Sreeranga, “Executing HOL Specifications: Towards an Evaluation Semantics for Classical Higher Order Logic”, In L. Claesen and M. Gordon, editors, Higher Order Logic Theorem Proving and its Applications. North-Holland, 1993.
Seger, C-J and Bryant, Randall, “Formal Verification of Digital Circuits by Sym bolic Evaluation of Partially Ordered Trajectories”, UBC Computer Science Department Technical Report 93-8, April 1993.
Bryant, Randall, “Formal Verification of Digital Circuits by Logic Simulation” Hardware Specification Verification and Synthesis: Mathematical Aspects: Proceedings / Mathematical Sciences Institute workshop, Cornell University Ithaca, New York, 1989; M.Leeser, G. Brown (eds.).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rajan, S., Joyce, J., Seger, C.CJ. (1994). From abstract data types to shift registers:. In: Joyce, J.J., Seger, CJ.H. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1993. Lecture Notes in Computer Science, vol 780. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57826-9_158
Download citation
DOI: https://doi.org/10.1007/3-540-57826-9_158
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57826-0
Online ISBN: 978-3-540-48346-5
eBook Packages: Springer Book Archive