Abstract
PVS stands for “Prototype Verification System.” It consists of a specification language integrated with support tools and a theorem prover. PVS tries to provide the mechanization needed to apply formal methods both rigorously and productively.
This tutorial serves to introduce PVS and its use in the context of hardware verification. In the first section, we briefly sketch the purposes for which PVS is intended and the rationale behind its design, mention some of the uses that we and others are making of it. We give an overview of the PVS specification language and proof checker. The PVS language, system, and theorem prover each have their own reference manuals, which you will need to study in order to make productive use of the system. A pocket reference card, summarizing all the features of the PVS language, system, and prover is also available.
The purpose of this tutorial is not to describe in detail the features of PVS and how to use the system. Rather, its purpose is to introduce some of the more unique and powerful capabilities that are provided by PVS and demonstrate how these features can be used in the context of hardware verification. We present completely worked out proofs of two hardware examples. One of the examples is a pipelined microprocessor that has been used as benchmark for model checkers and the other is a parameterized implementation of an N-bit ripple-carry adder.
S. Owre, N. Shankar, and J. M. Rushby. The PVS Specification Language (Beta Release). Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993.
Chapter PDF
References
Mark D. Aagard, Miriam E. Leeser, and Phillip J. Windley. Toward a super duper hardware tactic. In Proceedings of the HOL User's Group Workshop, pages 401–414, 1993.
Heather Alexander and Val Jones. Software Design and Prototyping using me too. Prentice Hall International, Hemel Hempstead, UK, 1990.
R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, New York, NY, 1979.
R. S. Boyer and J. S. Moore. A Computational Logic Handbook. Academic Press, New York, NY, 1988.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 220 states and beyond. In 5th Annual IEEE Symposium on Logic in Computer Science, pages 428–439, Philadelphia, PA, June 1990. IEEE Computer Society.
F. J. Cantu. Verifying an n-bit arithmetic logic unit. Blue book note 935, University of Edinburgh, June 1994.
R. L. Constable, et al. Implementing Mathematics with the Nuprl. Prentice-Hall, New Jersey, 1986.
T. Coquand and G. P. Huet. Constructions: A higher order proof system for mechanizing mathematics. In Proceedings of EUROCAL 85, Linz (Austria), Berlin, 1985. Springer-Verlag.
Costas Courcoubetis, editor. Computer-Aided Verification, CAV '93, volume 697 of Lecture Notes in Computer Science, Elounda, Greece, June/July 1993. Springer-Verlag.
D. Cyrluk, S. Rajan, N. Shankar, and M. K. Srivas. Effective theorem proving for hardware verification. In Ramayya Kumar and Thomas Kropf, editors, Preliminary Proceedings of the Second Conference on Theorem Provers in Circuit Design, pages 287–305, Bad Herrenalb (Blackforest), Germany, September 1994. Forschungszentrum Informatik an der Universität Karlsruhe, FZI Publication 4/94.
David Cyrluk. Microprocessor verification in PVS: A methodology and simple example. Technical Report SRI-CSL-93-12, Computer Science Laboratory, SRI International, Menlo Park, CA, December 1993.
N. G. de Bruijn. A survey of the project Automath. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 589–606. Academic Press, 1980.
B. Elspas, M. Green, M. Moriconi, and R. Shostak. A JOVIAL verifier. Technical report, Computer Science Laboratory, SRI International, January 1979.
W. M. Farmer, J. D. Guttman, and F. J. Thayer. IMPS: An interactive mathematical proof system. Technical Report M90-19, Mitre Corporation, 1991.
M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.
M. J. C. Gordon. HOL: A proof generating system for higher-order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 73–128. Kluwer, Dordrecht, The Netherlands, 1988.
Sharam Hekmatpour and Darrel Ince. Software Prototyping, Formal Methods, and VDM. International Computer Science Series. Addison-Wesley, Wokingham, England, 1988.
R. Kumar, K. Schneider, and T. Kropf. Structuring and automating hardware proofs in a higher-order therem proving environment. Formal Methods in System Design, 2(2):165–223, 1993.
Patrick Lincoln and John Rushby. Formal verification of an algorithm for interactive consistency under a hybrid fault model. In Courcoubetis [9], pages 292–304.
D. A. McAllester. ONTIC: A Knowledge Representation System for Mathematics. MIT Press, 1989.
W. McCune. Otter 2.0 users guide. Technical Report ANL-90/9, Argonne National Laboratory, 1990.
P. Michael Melliar-Smith and John Rushby. The Enhanced HDM system for specification and verification. In Proc. VerkShop III, pages 41–43, Watsonville, CA, February 1985. Published as ACM Software Engineering Notes, Vol. 10, No. 4, Aug. 85.
Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Some lessons learned. In J. C. P. Woodcock and P. G. Larsen, editors, FME '93: Industrial-Strength Formal Methods, pages 482–500, Odense, Denmark, April 1993. Volume 670 of Lecture Notes in Computer Science, Springer-Verlag.
W. Pase and M. Saaltink. Formal verification in m-EVES. In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Theorem Proving, pages 268–302, New York, NY, 1989. Springer-Verlag.
L. Robinson, K. N. Levitt, and B. A. Silverberg. The HDM Handbook. Computer Science Laboratory, SRI International, Menlo Park, CA, June 1979. Three Volumes.
Lawrence Robinson and Karl N. Levitt. Proof techniques for hierarchically structured programs. Communications of the ACM, 20(4):271–283, April 1976.
John Rushby, Friedrich von Henke, and Sam Owre. An introduction to formal specification and verification using Ehdm. Technical Report SRI-CSL-91-2, Computer Science Laboratory, SRI International, Menlo Park, CA, February 1991.
N. Shankar. Abstract datatypes in PVS. Technical Report SRI-CSL-93-9, Computer Science Laboratory, SRI International, Menlo Park, CA, December 1993.
Natarajan Shankar. Verification of real-time systems using PVS. In Courcoubetis [9], pages 280–291.
R. E. Shostak, R. Schwartz, and P. M. Melliar-Smith. STP: A mechanized logic for specification and verification. In D. Loveland, editor, 6th International Conference on Automated Deduction (CADE), New York, NY, 1982. Volume 138 of Lecture Notes in Computer Science, Springer-Verlag.
M.K. Srivas, et. al. Hardware verification using pvs: A tutorial. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA, 1994. A Forthcoming Technical Report.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Owre, S., Rushby, J.M., Shankar, N., Srivas, M.K. (1995). A tutorial on using PVS for hardware verification. In: Kumar, R., Kropf, T. (eds) Theorem Provers in Circuit Design. TPCD 1994. Lecture Notes in Computer Science, vol 901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59047-1_53
Download citation
DOI: https://doi.org/10.1007/3-540-59047-1_53
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59047-7
Online ISBN: 978-3-540-49177-4
eBook Packages: Springer Book Archive