SAT-Based Image Computation with Application in Reachability Analysis

摘要: Image computation finds wide application in VLSI CAD, such as state reachability analysis formal verification and synthesis, combinational verification, sequential test. Existing BDD-based symbolic algorithms for image are limited by memory resources practice, while SAT-based that can obtain the enumerating satisfying assignments to a CNF representation of Boolean relation potentially time resources. We propose new combine BDDs SAT order exploit their complementary benefits, offer mechanism trading off space vs. time. In particular, (1) our integrated algorithm uses represent input sets, formula relation, (2) fundamental enhancement called BDD Bounding is used whereby solver set dynamically changing prune search all solutions, (3) compute solutions below intermediate points decision tree, (4) fine-grained variable quantification schedule each subproblem, based on relation. These enhancements coupled with more engineering heuristics lead an overall handle larger problems. This supported preliminary results exact ISCAS benchmark circuits.