|
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
|
|