« back

edited by
Rolf Drechsler

Kluwer Academic Publishers
ISBN 1-4020-7721-1

Ordering:



For further information on the book and an overview of the contents
the preface is also available in pdf-format.



Book Summary:
Modern circuits may contain up to several hundred million transistors. In the meantime it has been observed that verification becomes the major bottleneck in design flows, i.e. up to 80% of the overall design costs are due to verification. This is one of the reasons why recently several methods have been proposed as alternatives to classical simulation. Simulation alone cannot guarantee sufficient coverage of the design resulting in bugs that may remain undetected.

As alternatives formal verification techniques have been proposed. Instead of simulating a design the correctness is proven by formal techniques. There are many different areas where these approaches can be used, like equivalence checking, property checking or symbolic simulation. Meanwhile these methods have been successfully applied in many industrial projects and have become the state-of-the-art technique in several fields. But the deployment of the existing tools in real-world projects also showed the weaknesses and problems of formal verification techniques. This gave motivating impulses for tool developers and researchers.

Advanced Formal Verification shows the latest developments in the verification domain from the perspectives of the user and the developer. World leading experts describe the underlying methods of today's verification tools and describe various scenarios from industrial practice. In the first part of the book the core techniques of today's formal verification tools, like SAT and BDDs are addressed. In addition, instances known to be difficult, like multipliers, are studied. The second part gives insight in professional tools and the underlying methodology, like property checking and assertion based verification. Finally, to cope with complete system on chip designs also analog components have to be considered.

In this book the state-of-the-art in many important fields of formal verification is described. Besides the description of the most recent research results, open problems and challenging research areas are addressed. Because of this, the book is intended for CAD developers and researchers in the verification domain, where formal techniques become a core technology to successful circuit and system design. Furthermore, the book is an excellent reference for users of verification tools to get a better understanding of the internal principles and by this to drive the tools to the highest performance. In this context the book is dedicated to all people in industry and academia to keep informed about the most recent developments in the field of formal verification.


Edited by:
Rolf Drechsler received his diploma and Dr. phil. nat. degree in computer science from the J.W. Goethe-University in Frankfurt am Main, Germany, in 1992 and 1995, respectively. He was with the Institute of Computer Science at the Albert-Ludwigs-University of Freiburg im Breisgau, Germany from 1995 to 2000. He joined the Corporate Technology Department of Siemens AG, Munich in 2000, where he worked as a Senior Engineer in the formal verification group. Since October 2001 he is with the University of Bremen, Germany, where he is now a full professor for computer architecture. He published five books at Kluwer Academic Publishers. His research interests include verification, logic synthesis, and evolutionary algorithms.

Contributing Authors of this Book

Table of Contents:

Introduction
by R. Drechsler.

1. Formal Verification.
2. Challenges.
3. Contributions to this Book.

1: What SAT-Solvers Can and Cannot Do
by E. Goldberg.

1. Introduction.
2. Hard Equivalence Checking CNF Formulas.
3. Stable Sets of Points.

2: Advancements in Mixed BDD and SAT Techniques
by G. Cabodi, S. Quer.

1. Introduction.
2. Background.
3. Comparing SAT and BDD Approaches: Are they Different?
4. Decision Diagrams as a Slave Engine in General SAT: Clause Compression by Means of ZBDDs.
5. Decision Diagram Preprocessing and Circuit-Based SAT.
6. Using SAT in Symbolic Reachability Analysis.
7. Conclusion, Remarks and Future Works.

3: Equivalence Checking of Arithmetic Circuits
by D. Stoffel, E. Karibaev, I. Kufareva, W. Kunz.

1. Introduction.
2. Verification Using Functional Properties.
3. Bit-Level Decision Diagrams.
4. Word-Level Decision Diagrams.
5. Arithmetic Bit-Level Verification.
6. Conclusion.
7. Future Perspectives.

4: Application of Property Checking
by R. Brinkmann, P. Johannsen, K. Winkelmann.

1. Circuit Verification Environment: User's View.
2. Circuit Verification Environment: Underlying Techniques.
3. Exploiting Symmetries.
4. Automated Data Path Scaling to Speed Up Property Checking.
5. Property Checking Use Cases.
6. Summary.

5: Assertion-Based Verification
by C.N. Coelho Jr, H.D. Foster.

1. Introduction.
2. Assertion Specification.
3. Assertion Libraries.
4. Assertion Simulation.
5. Assertions and Formal Verification.
6. Assertions and Synthesis.
7. PCI Property Specification Example.
8. Summary.

6: Formal Verification for Nonlinear Analog Systems
by W. Hartong, R. Klausen, L. Hedrich.

1. Introduction.
2. System Description.
3. Equivalence Checking.
4. Model Checking.
5. Summary.
6. Acknowledgement. Appendix: Mathematical Symbols