Image computation finds wide application in VLSI CAD, such as state reachability analysis in formal verification and synthesis, combinational verification, combinational and sequential test. Existing BDD-based symbolic algorithms for image computation are limited by the sensitivity of BDDs to the size and functionality of the Boolean expressions encountered. On the other hand, SAT-based algorithms that obtain the image by enumerating satisfying assignments to a CNF representation of the Boolean relation are potentially unable to traverse the entire solution space in a reasonable amount of time. We propose new algorithms that combine BDDs and SAT in order to overcome these drawbacks. In particular (1) BDDs and SAT are combined in a single integrated algorithm that uses BDDs to represent the input and image sets, and a CNF to represent the Boolean relation, (2) a fundamental enhancement called BDD Bounding is used in which the SAT solver uses the BDDs for the input set and the dynamically changing image set to prune the search space, (3) BDDs are used to compute all solutions at the leaves of the SAT decision tree, whenever the BDD sub-problem becomes manageable, (4) a very fine-grained variable quantification schedule is used based on the CNF representation of the transition relation. These enhancements coupled with more engineering heuristics lead to an overall algorithm that can potentially handle larger Boolean relations more robustly than before for image computation. This is supported by our preliminary results on exact reachability analysis of ISCAS benchmark circuits.
