Theorem Provers in Circuit Design: Theory, Practice and Experience Second International Conference, TPCD '94 Bad Herrenalb, Germany, September 26–28, 1994 Proceedings

Benchmark-circuits for hardware-verification....Pages 1-12
Reasoning about pipelines with structural hazards....Pages 13-32
A correctness model for pipelined microprocessors....Pages 33-51
Non-restoring integer square root: A case study in design by principled optimization....Pages 52-71
An automatic generalization method for the inductive proof of replicated and parallel architectures....Pages 72-91
A compositional circuit model and verification by composition....Pages 92-109
Exploiting structural similarities in a BDD-based verification method....Pages 110-125
Studies of the single pulser in various reasoning systems....Pages 126-145
Mechanized verification of speed-independence....Pages 146-164
Automatic correctness proof of the implementation of synchronous sequential circuits using an algebraic approach....Pages 165-184
Mechanized verification of refinement....Pages 185-202
Effective theorem proving for hardware verification....Pages 203-222
A formal framework for high level synthesis....Pages 223-238
Tutorial on design verification with synchronized transitions....Pages 239-257
A tutorial on using PVS for hardware verification....Pages 258-279
A reduced instruction set proof environment....Pages 280-285
Quantitative evaluation of formal based synthesis in ASIC design....Pages 286-291
Formal verification of characteristic properties....Pages 292-297
Extending formal reasoning with support for hardware diagrams....Pages 298-303