SAT based ATPG using fast justification and propagation in the implication graph

In this paper we present new methods for fast justification and propagation in the implication graph (IG) which is the core data structure of our SAT based implication engine. As the IG model rep-resents all information on the implemented logic function as well as the topology of a circuit, the proposed techniques inherit all advan-tages of both general SAT based and structure based approaches to justification, propagation, and implication. These three fundamen-tal Boolean problems are the main tasks to be performed during Automatic Test Pattern Generation (ATPG) such that the proposed algorithms are incorporated into our ATPG tool TIP which is built on top of the implication engine. Working exclusively in the IG, the complex functional operations of justification, propagation, and implication reduce to significantly simpler graph algorithms. They are easily extended to exploit bit-parallel techniques. As the IG is automatically generated for ar-bitrary logics the algorithms remain applicable independent of the required logic. This allows processing of various fault models us-ing the same engine. That is, the presented IG based methods offer a complete and versatile framework for rapid development of new ATPG tools that target emerging fault models such as cross-talk, delay or bridging faults. TIP currently handles stuck-at as well as various delay fault models. Furthermore, the proposed methods are used within tools for Boolean equivalence checking, optimization of netlists, timing analysis or retiming (reset state computation). In order to demonstrate the performance of IG based ATPG, i.e. justification and propagation in the IG, we provide experimental re-sults for stuck-at and path delay fault models. They show that TIP outperforms the state-of-the-art in SAT based and structure based ATPG.