|
" Theorem provers in circuit design : "
Ramayya Kumar, Thomas Kropf, eds.
| Document Type
|
:
|
BL
|
| Record Number
|
:
|
746390
|
| Doc. No
|
:
|
b566339
|
| Main Entry
|
:
|
Ramayya Kumar, Thomas Kropf, eds.
|
| Title & Author
|
:
|
Theorem provers in circuit design : : theory, practice, and experience : second international conference, TPCD '94, Bad Herrenalb, Germany, September 26-28, 1994 : proceedings\ Ramayya Kumar, Thomas Kropf, eds.
|
| Publication Statement
|
:
|
Berlin ; New York : Springer-Verlag, ©1995.
|
| Series Statement
|
:
|
Lecture notes in computer science, 901.
|
| Page. NO
|
:
|
viii, 303 pages : illustrations ; 24 cm.
|
| ISBN
|
:
|
0387590471
|
|
|
:
|
: 3540491775
|
|
|
:
|
: 3540590471
|
|
|
:
|
: 9780387590479
|
|
|
:
|
: 9783540491774
|
|
|
:
|
: 9783540590477
|
| Contents
|
:
|
Benchmark-circuits for hardware-verification / Thomas Kropf --; Reasoning about pipelines with structural hazards / Mark Aagaard and Miriam Leeser --; A correctness model for pipelined microprocessors / Phillip J. Windley and Michael L. Coe --; Non-restoring integer square root : a case study in design by principled optimization / John O'Leary [and others] --; An automatic generalization method for the inductive proof of replicated and parallel architectures / Laurence Pierre --; A compositional circuit model and verification by composition / Zheng Zhu --; Exploiting structural similarities in a BDD-based verification method / C.A.J. van Eijk and G.L.J.M. Janssen --; Studies of the single pulser in various reasoning systems / Steven D. Johnson, Paul S. Miner and Albert Camilleri --; Mechanized verification of speed-independence / Michael Kishinevsky and Jørgen Staunstrup --; Automatic correctness proof of the implementation of synchronous sequential circuits using an algebraic approach / Junji Kitamichi [and others] --; Mechanized verification of refinement / Niels Maretti --; Effective theorem proving for hardware verfication / D. Cyrluk [and others] --; A formal framework for high level synthesis / Thomas Kropf, Klaus Schneider and Ramayya Kumar --; Tutorial design verification with synchronized transitions / Niels Mellergaard and Jørgen Staunstrup --; A tutorial on using PVS for hardware verification / S. Owre [and others] --; A reduced instruction set proof environment / Holger Busch --; Quantitative evaluation of formal based synthesis in ASIC design / G. Bezzi [and others] --; Formal verification of characteristic properties / Michel Allemand --; Extending formal reasoning with support for hardware diagrams / Kathi Fisler.
|
| Subject
|
:
|
Automatic theorem proving -- Congresses.
|
| Subject
|
:
|
Automatic theorem proving.
|
| Subject
|
:
|
Digital integrated circuits -- Computer-aided design -- Congresses.
|
| LC Classification
|
:
|
TK7874.65R363 1995
|
| Added Entry
|
:
|
Ramayya Kumar
|
|
|
:
|
Thomas Kropf
|
| Parallel Title
|
:
|
TPCD '94
|
| |