Correct Hardware Design and Verification Methods

1. Front Matter

   Pages I-XI

   PDF

2. Invited Talks

   1. Esterel and Jazz : Two Synchronous Languages for Circuit Design

      • Gérard Berry

      Pages 1-1

   2. Design Process of Embedded Automotive Systems—Using Model Checking for Correct Specifications

      • Peter Jansen

      Pages 2-7

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

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.

• Hardware
• formal method
• microprocessor
• model
• model checking
• simulation
• theorem proving
• verification
• complexity

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

  Laurence Pierre

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

  Thomas Kropf

Policies and ethics