Skip to main content
SpringerLink
Log in

Correct Hardware Design and Verification Methods

10th IFIP WG10.5 Advanced Research Working Conference, CHARME'99, Bad Herrenalb, Germany, September 27-29, 1999, Proceedings

  • Conference proceedings
  • © 1999

Overview

Editors:
  1. Laurence Pierre

    1. CMI/Université de Provence, Marseille Cedex 13, France

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Thomas Kropf

    1. Technische Informatik, Universität Tübingen, Tübingen, Germany

    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 1703)

Included in the following conference series:

Conference proceedings info: CHARME 1999.

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

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
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

Table of contents (34 papers)

  1. Front Matter

    Pages I-XI
    Download chapter PDF

  3. Proof of Microprocessors

    1. A Proof of Correctness of a Processor Implementing Tomasulo’s Algorithm without a Reorder Buffer

      • Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam Srivas
      Pages 8-22

    2. Formal Verification of Explicitly Parallel Microprocessors

      • Byron Cook, John Launchbury, John Matthews, Dick Kieburtz
      Pages 23-36

    3. Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic

      • Miroslav N. Velev, Randal E. Bryant
      Pages 37-53

  4. Model Checking

    1. Model Checking TLA+ Specifications

      • Yuan Yu, Panagiotis Manolios, Leslie Lamport
      Pages 54-66

    2. Efficient Decompositional Model Checking for Regular Timing Diagrams

      • Nina Amla, E. Allen Emerson, Kedar S. Namjoshi
      Pages 67-81

    3. Vacuity Detection in Temporal Model Checking

      • Orna Kupferman, Moshe Y. Vardi
      Pages 82-98

  5. Formal Methods and Industrial Applications

    1. Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard

      • Cindy Eisner
      Pages 99-109

    2. Practical Application of Formal Verification Techniques on a Frame Mux/Demux Chip from Nortel Semiconductors

      • Y. Xu, E. Cerny, A. Silburt, A. Coady, Y. Liu, P. Pownall
      Pages 110-124

    3. Efficient Verification of Timed Automata Using Dense and Discrete Time Semantics

      • Marius Bozga, Oded Maler, Stavros Tripakis
      Pages 125-141

  6. Abstraction and Compositional Techniques

    1. From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking

      • E. Allen Emerson, 1]Richard J. Trefler
      Pages 142-157

    2. Automatic Error Correction of Large Circuits Using Boolean Decomposition and Abstraction

      • Dirk W. Hoffmann, Thomas Kropf
      Pages 157-172

    3. Abstract BDDs: A Technique for Using Abstraction in Model Checking

      • Edmund Clarke, Somesh Jha, Yuan Lu, Dong Wang
      Pages 172-187

  7. Theorem Proving Related Approaches

    1. Formal Synthesis at the Algorithmic Level

      • Christian Blumenröhr, Viktor Sabelfeld
      Pages 187-202

    2. Xs Are for Trajectory Evaluation, Booleans Are for Theorem Proving

      • Mark D. Aagaard, Thomas F. Melham, John W. O’Leary
      Pages 202-218

    3. Verification of Infinite State Systems by Compositional Model Checking

      • K. L. McMillan
      Pages 219-237

  8. Symbolic Simulation/Symbolic Traversal

    1. Formal Verification of Designs with Complex Control by Symbolic Simulation

      • Gerd Ritter, Hans Eveking, Holger Hinrichsen
      Pages 238-250

    2. Hints to Accelerate Symbolic Traversal

      • Kavita Ravi, Fabio Somenzi
      Pages 250-266
Back to top

Other volumes

  1. Correct Hardware Design and Verification Methods

Keywords

About this book

CHARME’99 is the tenth in a series of working conferences devoted to the dev- opment and use of leading-edge formal techniques and tools for the design and veri?cation of hardware and systems. Previous conferences have been held in Darmstadt (1984), Edinburgh (1985), Grenoble (1986), Glasgow (1988), Leuven (1989), Torino (1991), Arles (1993), Frankfurt (1995) and Montreal (1997). This workshop and conference series has been organized in cooperation with IFIP WG 10. 5. It is now the biannual counterpart of FMCAD, which takes place every even-numbered year in the USA. The 1999 event took place in Bad Her- nalb, a resort village located in the Black Forest close to the city of Karlsruhe. The validation of functional and timing behavior is a major bottleneck in current VLSI design systems. A predominantly academic area of study until a few years ago, formal design and veri?cation techniques are now migrating into industrial use. The aim of CHARME’99 is to bring together researchers and users from academia and industry working in this active area of research. Two invited talks illustrate major current trends: the presentation by G´erard Berry (Ecole des Mines de Paris, Sophia-Antipolis, France) is concerned with the use of synchronous languages in circuit design, and the talk given by Peter Jansen (BMW, Munich, Germany) demonstrates an application of formal methods in an industrial environment. The program also includes 20 regular presentations and 12 short presentations/poster exhibitions that have been selected from the 48 submitted papers.

Editors and Affiliations

  • CMI/Université de Provence, Marseille Cedex 13, France

    Laurence Pierre

  • Technische Informatik, Universität Tübingen, Tübingen, Germany

    Thomas Kropf

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation