TABLE OF CONTENTS Part 3 continues to focus on the portion of the Verification Cycle that focusses on the development of the Verification Environment. While simulation-based verification is the most widely used method of functional verification, formal verification continues to grow and meld with mainstream design efforts. In the past, formal verification was hampered by size constraints and language complexity, but advances on both fronts have opened the gates to widespread usage of formal techniques in functional verification.
Chapters 11 and 12 introduce formal verification, discuss the algorithms behind the methodology, and describe the Property Specification Language (PSL/Sugar). Major portions of the text are devoted to Boolean Equivalency Checking and Property Checking, the most widely used formal methodologies. Chapter 12 also includes a description of semi-formal verification, a leading method that melds formal techniques with simulation based methodologies.
In simulation, the verification environment visits one state of the design under verification (DUV) at a time. This process can be viewed as state traversal. The set of all possible states for a DUV is called its reachable state space. The overwhelming size of the DUV's state space is the biggest verification challenge (Section 1.1). Throughout this book, the main technique underlying all verification tasks is simulation of the DUV. However, there are severe limitations of this approach that will be discussed now.
At every state visited during simulation, checkers and monitors are active to...
