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.

The book shows latest developments in the verification domain from

the user and from the developer perspective. 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.

By 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.