This title is printed to order. This book may have been self-published. If so, we cannot guarantee the quality of the content. In the main most books will have gone through the editing process however some may not. We therefore suggest that you be aware of this before ordering this book. If in doubt check either the author or publisher’s details as we are unable to accept any returns unless they are faulty. Please contact us if you have any questions.
This text contains two distinct, but related, approaches to the verification problem. Both are based on symbolic simulation. The first approach is applied at the gate level and has been successful in verifying sub-circuits of industrial microprocessors with tens and even hundreds of thousands of gates. The second approach is applied at a high-level of abstraction and is used for high-level descriptions of designs. Historically, it has been difficult to apply formal verification methods developed in academia to the verification problems encountered in commercial design projects. This book describes new ideas that enable the use of formal methods, specifically symbolic simulation, in validating commercial hardware designs of remarkable complexity. These ideas are demonstrated on circuits with many thousands of latches-much larger circuits than those previously formally verified. The book contains three main topics: self-consistency, a technique for deriving a formal specification of design behaviour from the design itself; the use of the parametric representation to encode predicates as functional vectors for symbolic simulation, an important step in addressing the state-explosion problem; and incremental flushing, a method used to verify high-level descriptions of out-of-order execution. The book concludes with work on verification of simplified models of out-of-order processors.
