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.--publisher's Website. 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. Ramayya Kumar, Thomas Kropf, Eds. Includes Bibliographical References. 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 Although having many drawbacks, benchmark circuits allow a more succinct and direct comparison of different approaches for solving a certain problem. Second International Conference, TPCD '94, Bad Herrenalb, Germany, September 26 - 28, 1994. Proceedings