SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

A Tutorial on Using PVS for Hardware Verification
 by Sam Owre, Dr. John Rushby, Dr. Natarajan Shankar & M. K. Srivas.

Lecture Notes in Computer Science, Volume 901.
From Theorem Provers in Circuit Design (TPCD '94).
Edited by Ramayya Kumar and Thomas Kropf.
Springer-Verlag, Bad Herrenalb, Germany.
September, 1994.
Pages 258–279.


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.

BibTEX Entry
@inproceedings{tpcd94-tutorial,
  AUTHOR = {{S.} Owre and {J.} {M.} Rushby and {N.} Shankar and {M.} {K.} Srivas},
  TITLE = {{A} Tutorial on Using {PVS} for Hardware Verification},
  BOOKTITLE = {Theorem Provers in Circuit Design (TPCD '94)},
  YEAR = {1994},
  EDITOR = {Ramayya Kumar and Thomas Kropf},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {901},
  PAGES = {258--279},
  ADDRESS = {Bad Herrenalb, Germany},
  MONTH = {sep},
  PUBLISHER = {Springer-Verlag},
  URL = {http://www.csl.sri.com/papers/tpcd94-tutorial/}
}
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy