Correct Hardware Design and Verification Methods: 10th Ifip Wg I 0.5 Advanced Research Working Conference, Charme'99, Bad Herrenalb, Germany, September 27-29, 1999, Proceedings

by Charme'9 (1999 Bad Herrenalb, Germany); Goos, G.; Hartmanis, J.; Leeuwen, J. Van; Pierre, Laurence

• ISBN13: 9783540665595
• ISBN10: 3540665595
• Format: Paperback
• Copyright: 1999-06-01
• Publisher: Springer Verlag

Summary

This book constitutes the refereed proceedings of the 10th IFIP WG10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME'99, held in Bad Herrenalb, Germany in September 1999. The 20 revised full papers and 12 revised short papers presented together with two invited contributions were carefully reviewed and selected from 48 papers submitted. The papers are organized in topical sections on proofs of microprocessors, model checking, formal methods and industrial applications, abstraction and compositional techniques, theorem proving and related approaches, symbolic simulation and symbolic traversal, and specification languages and methodologies.

Table of Contents

Invited Talks
Esterel and Jazz Two Synchronous Languages for Circuit Design	p. 1
Design Process of Embedded Automotive Systems - Using Model Checking for Correct Specifications	p. 2
Proof of Microprocessors
A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm without a Reorder Buffer	p. 8
Formal Verification of Explicitly Parallel Microprocessors	p. 23
Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic	p. 37
Model Checking
Model Checking TLA+ Specifications	p. 54
Efficient Decompositional Model-Checking for Regular Timing Diagrams	p. 67
Vacuity Detection in Temporal Model Checking	p. 82
Formal Methods and Industrial Applications
Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard	p. 97
Practical Application of Formal Verification Techniques on a Frame Mux/Demux Chip from Nortel Semiconductors	p. 110
Efficient Verification of Timed Automata Using Dense and Discrete Time Semantics	p. 125
Abstraction and Compositional Techniques From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking	p. 142
Automatic Error Correction of Large Circuits Using Boolean Decomposi- tion and Abstraction	p. 157
Abstract BDDs: A Technique for Using Abstraction in Model Checking	p. 172
Theorem Proving Related Approaches
Formal Synthesis at the Algorithmic Level	p. 187
Xs Are for Trajectory Evaluation, Booleans Are for Theorem Proving	p. 202
Verification of Infinite State Systems by Compositional Model Checking	p. 219
Symbolic Simulation/Symbolic Traversal
Formal Verification of Designs with Complex Control by Symbolic Simulation	p. 234
Hints to Accelerate Symbolic Traversal	p. 250
Specification Languages and Methodologies
Modeling and Checking Networks of Communicating Real-Time Processes	p. 265
"Have I Written Enough Properties?" A Method of Comparison between Specification and Implementation	p. 280
Program Slicing of Hardware Description Languages	p. 298
Posters
Results of the Verification of a Complex Pipelined Machine Model	p. 313
Hazard-Freedom Checking in Speed-Independent Systems	p. 317
Yet Another Look at LTL Model Checking	p. 321
Verification of Finite-State-Machine Refinements Using a Symbolic Methodology	p. 326
Refinement and Property Checking in High-Level Synthesis Using Attribute Grammars	p. 330
A Systematic Incrementalization Technique and Its Application to Hardware Design	p. 334
Bisimulation and Model Checking	p. 338
Circular Compositional Reasoning about Liveness	p. 342
Symbolic Simulation of Microprocessor Models Using Type Classes in Haskell	p. 346
Exploiting Retiming in a Guided Simulation Based Validation Methodology	p. 350
Fault Models for Embedded Systems	p. 354
Validation of Object-Oriented Concurrent Designs by Model Checking	p. 360
Author Index	p. 365
Table of Contents provided by Publisher. All Rights Reserved.