Hardware Design Verification

Chapter 8. Chapter Highlights Binary decision diagramsDecision diagram variantsDecision diagram-based equivalence checkingBoolean satisfiabilitySymbolic simulation A fundamental problem in formal verification is determining whether two Boolean fu...

8.1. A BDD is a directed acyclic graph (DAG) that represents a Boolean function. A node in a BDD is associated with a Boolean variable and has two outgoing edges. One edge represents the TRUE (1) value of the variable, and the other, the FALSE (0) ...

8.2. In this section we will study several variants of decision diagrams, all of which are canonical and have efficient manipulation algorithms, such as construction and Boolean operations. Each variant is targeted toward a specific application dom...

8.3. In this section we will study the use of BDDs in determining the functional equivalence of two Boolean functions or circuits, known as equivalence checking. The ideas presented here are applicable not only to BDDs but also to any canonical dec...

8.4. An alternative to BDDs in checking equivalence uses techniques from determining Boolean satisfiability called SAT. The problem of Boolean satisfiability decides whether a Boolean expression or formula is identically equal to 1. That is, it is ...

8.5. With traditional simulation, stimuli as well as responses consist of bits of binary constants. In a combinational circuit with n input bits, the input space has 2n vectors, or points. A traditional simulator simulates one point at a time. On t...

8.6. We started the chapter with decision diagrams. First, the BDD was studied. We showed how to construct a BDD and reduce it to canonical form. The reduction procedure consists of two steps: removing nodes with both edges that point to the same n...

8.7. 1For the BDD in Figure 8.44, do the following: Is the BDD reduced?Derive the function represented by the BDD in sum-of-products form.Repeat (b) for product of sums. Figure 8.44. BDD for obtaining sum-of-products and product-of-sums ...