Efficient Formal Design Verification: Data Structure + Algorithms

We describe a data structure and a set of BDD based algorithms for efficient formal design verification. We argue that hardware designs should be translated into an intermediate hierarchical netlist of combinational tables and sequential elements, and internally represented by a flattened network of gates and latches, akin to that in SIS [32]. We establish that the core computation in BDD based formal design verification is forming the image and pre-image of sets of states under the transition relation characterizing the design. To make this step efficient, we address BDD variable ordering, use of partitioned transition relations, use of clustering, use of don't cares, and redundant latch removal. Many of these techniques have been studied in the past. We provide a complete integrated set of modified algorithms and give references andcomparisons with previous work. We report experimental results on a series of seven industrial examples containing from 28 to 172 binary valued latches. ..