Efficient reachability checking using sequential SAT

Reachability checking and preimage computation are fundamental problems in ATPG and formal verification. Traditional sequential search techniques based on ATPG/SAT, or on OBDDS have diverging strengths and weaknesses. Here, we describe how structural analysis and conflict-based learning are combined in order to improve the efficiency of sequential search. We use conflict-based learning and illegal state learning across time-frames. We also address issues in efficiently bounding the search space in a single time-frame and across time-frames. We analyze each of these techniques experimentally and demonstrate the advantages of each technique. We compare performance against a commercial sequential ATPG engine and VIS [RK. Brayton et al., (1996)] on a set of standard benchmarks.