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

This volume presents the proceedings of the Second International Conference on Theorem Provers in Circuit Design (TPCD '94) jointly organized by the Forschungszentrum Informatik (University of Karlsruhe) and IFIP Working Group 10.2 in Bad Herrenalb, Germany in September 1994.
The 19 papers included are thoroughly revised versions of the submissions selected for presentation at the conference and address all current aspects of theorem provers in circuit design. Particular emphasis is given to benchmark-circuits for hardware verification; tutorials on two popular theorem provers are included.

---

This volume presents the proceedings of the Second International Conference on Theorem Provers in Circuit Design (TPCD '94) jointly organized by the Forschungszentrum Informatik (University of Karlsruhe) and IFIP Working Group 10.2 in Bad Herrenalb, Germany in September 1994.
The 19 papers included are thoroughly revised versions of the submissions selected for presentation at the conference and address all current aspects of theorem provers in circuit design. Particular emphasis is given to benchmark-circuits for hardware verification; tutorials on two popular theorem provers are included.

---

This volume presents the proceedings of the Second International Conference on Theorem Provers in Circuit Design (TPCD '94) jointly organized by the Forschungszentrum Informatik (University of Karlsruhe) and IFIP Working Group 10.2 in Bad Herrenalb, Germany in September 1994.
The 19 papers included are thoroughly revised versions of the submissions selected for presentation at the conference and address all current aspects of theorem provers in circuit design. Particular emphasis is given to benchmark-circuits for hardware verification; tutorials on two popular theorem provers are included.
Content:
Front Matter....Pages -
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
Back Matter....Pages -

---

This volume presents the proceedings of the Second International Conference on Theorem Provers in Circuit Design (TPCD '94) jointly organized by the Forschungszentrum Informatik (University of Karlsruhe) and IFIP Working Group 10.2 in Bad Herrenalb, Germany in September 1994.
The 19 papers included are thoroughly revised versions of the submissions selected for presentation at the conference and address all current aspects of theorem provers in circuit design. Particular emphasis is given to benchmark-circuits for hardware verification; tutorials on two popular theorem provers are included.
Content:
Front Matter....Pages -
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
Back Matter....Pages -
....