Lecture Notes in Computer Science, Volume 901.
From Theorem Provers in Circuit Design (TPCD '94).
Springer-Verlag, Bad Herrenalb, Germany.
September, 1994.
Pages 203–222.

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 off-the-shelf BDD-based propositional simplifier. These automatic procedures can be combined into general-purpose 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 N-bit adder, the Saxe pipelined processor, and the benchmark Tamarack microprocessor design. These examples illustrate the basic design philosophy underlying PVS where powerful and efficient low-level inferences are employed within high-level user-defined proof strategies. This approach is contrasted with approaches based on tactics or batch-oriented theorem proving.

@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 = {203--222},
    ADDRESS = {Bad Herrenalb, Germany},
    MONTH = {sep},
    PUBLISHER = {Springer-Verlag},
    URL = {http://www.csl.sri.com/papers/tpcd94/}
}

• tpcd94.pdf
• tpcd94.ps