SAT-Based Image Computation with Application in Reachability Analysis

Image computation nds wide application in VLSI CAD, such as state reachability analysis in formal veri cation and synthesis, combinational veri cation, combinational and sequential test. Existing BDD-based symbolic algorithms for image computation are limited by memory resources in practice, while SAT-based algorithms that can obtain the image by enumerating satisfying assignments to a CNF representation of the Boolean relation are potentially limited by time resources. We propose new algorithms that combine BDDs and SAT in order to exploit their complementary bene ts, and to o er a mechanism for trading o space vs. time. In particular, (1) our integrated algorithm uses BDDs to represent the input and image sets, and a CNF formula to represent the Boolean relation, (2) a fundamental enhancement called BDD Bounding is used whereby the SAT solver uses the BDDs for the input set and the dynamically changing image set to prune the search space of all solutions, (3) BDDs are used to compute...

• Type: Conference
• Year: 2000
• Where: FMCAD
• Authors: Aarti Gupta, Zijiang Yang, Pranav Ashar, Anubhav Gupta
• Keywords: Boolean Relation, Combinational Veri Cation, FMCAD 2000, Formal Methods, Veri Cation