IGRAINE - An implication GRaph-bAsed engINE for fast implication, justification, and propagation

Implication, justification, and propagation are three important Boolean pro blems that have to be solved during many tasks in electronic design automat ion (EDA) for digital circuits. As they constitute the key components of au tomatic test pattern generation (ATPG) most algorithms that tackle these pr oblems originate in ATPG research. Due to their fundamental nature these AT PG-based methods have successfully been adopted by logic synthesis and form al verification where they have helped advance the fields of netlist optimi zation and Boolean equivalence checking. Despite their high importance and wide applicability, the data structures a nd algorithms suggested so far have proven to be suboptimal and inflexible in several respects. Therefore, we propose IGRAINE, a fast and flexible eng ine for performing implication, justification, and propagation in combinati onal circuits that is specifically optimized with respect to these tasks. D ue to its modular design, IGRAINE is easily included into new applications that require ATPG-based methods. Our approach is based on a new implication graph (IG) model which forms the core of IGRAINE. Contrary to other IG mod els, the proposed IG represents all information on the implemented logic fu nction as well as the topology of a combinational circuit in a single graph model. So, the proposed techniques inherit all advantages of both general SAT based and structure based approaches to justification, propagation, and implication. Working exclusively in the IG, the complex functional operati ons of justification, propagation, and implication reduce to significantly simpler graph algorithms. IGRAINE evaluates implications by a partial trave rsal of the IG and derives indirect implications by graph analysis. Justifi cation and propagation are solved by a guided traversal of the IG. These gr aph algorithms allow the effective exploitation of various bit-parallel tec hniques. As the IG is automatically generated for arbitrary logics the pres ented algorithms remain applicable independent of the required logic. This allows, for example, processing of various fault models using the same core engine. That is, our IG-based methods offer a complete and versatile frame work for rapid development of new ATPG tools that target emerging fault mod els such as cross-talk, delay, or bridging faults. Our ATPG tool TIP is bui lt on top of IGRAINE. It currently handles stuck-at as well as various dela y fault models. TIP has also been extended to solve Boolean equivalence che cking using Ic-based techniques. Furthermore, the proposed methods are used within tools for optimization of netlists, functional timing analysis, or retiming (reset state computation). In order to demonstrate the performance of the presented IG based algorithm s for implication, justification, and propagation, we provide experimental results for stuck-at and path delay fault ATPG as well as Boolean equivalen ce checking. They show that TID outperforms the state-of-the-art in SAT-bas ed and structure-based ATPG. A comparison with tools for Boolean equivalenc e checking demonstrates the high effectiveness of our approach.