Forward image computation with backtracing ATPG and incremental state-set construction
Kameshwar Chandrasekar, Michael S. Hsiao · 2005
Image computation is a fundamental step in formal verification of sequential systems, including sequential equivalence checking and symbolic model checking. Since conventional Reduced Ordered Binary Decision Diagram (ROBDD) based methods can potentially suffer from memory explosion, there has been a growing interest in using Automatic Test Pattern Generation (ATPG) / Boolean Satisfiability (SAT) based techniques in recent years. While ATPG has been successful for computing pre-image, image computation presents a very different set of problems. In this paper, we present a novel backtracing-based ATPG technique for forward image computation. We carefully alter the ATPG engine to compute the image cubes and store them incrementally in a Zero-Suppressed Binary Decision Diagram (ZBDD). In order to improve the efficiency of image computation, we propose three heuristics: (i) gate-observability based decision selection heuristics to accelerate ATPG, (ii) search-state based learning techniques supported with a proof for correctness, and (iii) on-the-fly state-set minimization techniques to reduce the size of computed image set. Experimental results on ISCAS '89 and ITC '99 benchmark circuits show that we can achieve orders of magnitude improvement over OBDD-based and SAT-based techniques.