Sciweavers

Share
FMCAD
2000
Springer

SAT-Based Image Computation with Application in Reachability Analysis

10 years 6 months ago
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...
Aarti Gupta, Zijiang Yang, Pranav Ashar, Anubhav G
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where FMCAD
Authors Aarti Gupta, Zijiang Yang, Pranav Ashar, Anubhav Gupta
Comments (0)
books