This book examines formal verification that validates the implementation of a chip design with respect to its specification by applying mathematical proofs. Chip capacity follows Moore's law, and chips are commonly produced at the time of this writing with over 70 million gates per device. However, ensuring correct functional behavior of such large designs becomes more and more challenging.
Formal techniques have been commercialized in the last 10 years. In Chapter 2, we introduce basic data structures and concepts in formal verification, such as Binary Decision Diagrams (BDD) and the SAT and Image/Pre-Image computation algorithms. We then describe some advanced algorithms that improve performance of formal verification.
In Chapter 3, we introduce basic concepts and characteristics of different simulation approaches, such as delay modeling, simulation values modeling, and fault modeling. Simulation can validate all possible behaviors of a design in a brute-force manner. However, rapidly evolving markets demand short design cycles while the increasing complexity of a design necessarily dictates that simulation coverage is less and less complete. Formal verification itself cannot solely accomplish the validation task. Thus, combining different approaches together to serve the purpose of validation of digital circuits is desirable. Chapter 4 of this book focuses on the Integrated Design Validation (IDV) system that develops an integrated framework for design validation and takes advantage of current technology in the areas of simulation and formal verification resulting in a practical validation engine with reasonable runtime. In Chapter 4, we introduce the key components in the IDV system; the circuit complexity analyzer, the partitioning tool based upon design hierarchy, as well as coverage analysis methods that compute a degree of design validation and invoke methods for intelligently updating the partitioning tool for further validation iterations.
Table of Contents: Introduction / Formal Methods Background / Simulation Technologies / Integrated Design Validation System / Conclusions / References