
Effective Theorem Proving for Hardware Verification
by Dr. Natarajan Shankar, D. Cyrluk, S. Rajan & M.K. Srivas.
Lecture Notes in Computer Science, Volume 901. From Theorem Provers in Circuit Design (TPCD '94). SpringerVerlag, Bad Herrenalb, Germany. September, 1994. Pages 203–222.
Abstract
The attractiveness of using theorem provers for system design verification lies in their generality. The major practical challenge confronting theorem proving technology is in combining this generality with an acceptable degree of automation. We describe an approach for enhancing the effectiveness of theorem provers for hardware verification through the use of efficient automatic procedures for rewriting, arithmetic and equality reasoning, and an offtheshelf BDDbased propositional simplifier. These automatic procedures can be combined into generalpurpose proof strategies that can efficiently automate a number of proofs including those of hardware correctness. The inference procedures and proof strategies have been implemented in the PVS verification system. They are applied to several examples including an Nbit adder, the Saxe pipelined processor, and the benchmark Tamarack microprocessor design. These examples illustrate the basic design philosophy underlying PVS where powerful and efficient lowlevel inferences are employed within highlevel userdefined proof strategies. This approach is contrasted with approaches based on tactics or batchoriented theorem proving.
BibT_{E}X Entry
@inproceedings{tpcd94,
AUTHOR = {{D.} Cyrluk and {S.} Rajan and {N.} Shankar and and {M.K.} Srivas},
TITLE = {Effective Theorem Proving for Hardware Verification},
BOOKTITLE = {Theorem Provers in Circuit Design (TPCD '94)},
YEAR = {1994},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {901},
PAGES = {203222},
ADDRESS = {Bad Herrenalb, Germany},
MONTH = {sep},
PUBLISHER = {SpringerVerlag},
URL = {http://www.csl.sri.com/papers/tpcd94/}
}
Files

