Improved SAT-based bounded reachability analysis

Symbolic simulation is widely used in logic verification. Previous approaches based on BDDs suffer from space outs, while SAT-based approaches have been found fairly robust. We propose a SAT-based symbolic simulation algorithm using a noncanonical two-input AND/INVERTER graph representation and on-the-fly reduction algorithm on such a graph representation. Unlike previous approaches where circuit is explicitly unrolled, we propagate the symbolic values represented using the simplified AND/INVERTER graph across the time frames. This simplification have significant impact on the performance of SAT-solver. Experimental results on large examples show the effectiveness of the proposed technique over previous approaches. Specifically we were able to find real bugs in pieces of the designs from IBM Gigahertz Processor Project which were previously remained undetected. Moreover, previous heuristics used in BDD-based symbolic simulation can still be applied to this algorithm