Efficient reachability checking using sequential SAT
G. Parthasarathy, M.K. Iyer, Kwang-Ting Tim Cheng, Li-C. Wang · Asia and South Pacific Design Automation Conference · 2004
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.