[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Theorem Provers in Circuit Design: Theory, Practice and Experience

Second International Conference, TPCD '94, Bad Herrenalb, Germany, September 26-28, 1994. Proceedings

  • Conference proceedings
  • © 1995

Overview

Editors:
  1. Ramayya Kumar
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Thomas Kropf
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 901)

Included in the following conference series:

Conference proceedings info: TPCD 1994.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

About this book

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.

Similar content being viewed by others

Keywords

Table of contents (19 papers)

  1. Front Matter

    Download chapter PDF

  2. Benchmark-circuits for hardware-verification

    • Thomas Kropf
    Pages 1-12

  3. Reasoning about pipelines with structural hazards

    • Mark Aagaard, Miriam Leeser
    Pages 13-32

  4. A correctness model for pipelined microprocessors

    • Phillip J. Windley, Michael L. Coe
    Pages 33-51

  5. Non-restoring integer square root: A case study in design by principled optimization

    • John O'Leary, Miriam Leeser, Jason Hickey, Mark Aagaard
    Pages 52-71

  6. An automatic generalization method for the inductive proof of replicated and parallel architectures

    • Laurence Pierre
    Pages 72-91

  7. A compositional circuit model and verification by composition

    • Zheng Zhu
    Pages 92-109

  8. Exploiting structural similarities in a BDD-based verification method

    • C. A. J. van Eijk, G. L. J. M. Janssen
    Pages 110-125

  9. Studies of the single pulser in various reasoning systems

    • Steven D. Johnson, Paul S. Miner, Albert Camilleri
    Pages 126-145

  10. Mechanized verification of speed-independence

    • Michael Kishinevsky, Jørgen Staunstrup
    Pages 146-164

  11. Automatic correctness proof of the implementation of synchronous sequential circuits using an algebraic approach

    • Junji Kitamichi, Sumio Morioka, Teruo Higashino, Kenichi Taniguchi
    Pages 165-184

  12. Mechanized verification of refinement

    • Niels Maxetti
    Pages 185-202

  13. Effective theorem proving for hardware verification

    • D. Cyrluk, S. Rajan, N. Shankar, M. K. Srivas
    Pages 203-222

  14. A formal framework for high level synthesis

    • Thomas Kropf, Klaus Schneider, Ramayya Kumar
    Pages 223-238

  15. Tutorial on design verification with synchronized transitions

    • Niels Mellergaard, Jørgen Staunstrup
    Pages 239-257

  16. A tutorial on using PVS for hardware verification

    • S. Owre, J. M. Rushby, N. Shankar, M. K. Srivas
    Pages 258-279

  17. A reduced instruction set proof environment

    • Holger Busch
    Pages 280-285

  18. Quantitative evaluation of formal based synthesis in ASIC design

    • G. Bezzi, M. Bombana, P. Cavalloro, S. Conigliaro, G. Zaza
    Pages 286-291

  19. Formal verification of characteristic properties

    • Michel Allemand
    Pages 292-297

  20. Extending formal reasoning with support for hardware diagrams

    • Kathi Fisler
    Pages 298-303
Back to top

Other volumes

  1. Theorem Provers in Circuit Design

Bibliographic Information

Publish with us

Policies and ethics

Back to top