A Tutorial on Using PVS for Hardware Verification

PVS stands for "Prototype Verification System." It consists of a specication 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 hard-ware verification. In the rst 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 o