A SAT-based implication engine for efficient ATPG, equivalence checking, and optimization of netlists
- 1 January 1997
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10923152,p. 648-655
- https://doi.org/10.1109/iccad.1997.643607
Abstract
The paper presents a flexible and efficient approach to evaluating implications as well as deriving indirect implications in logic circuits. Evaluation and derivation of implications are essential in ATPG, equivalence checking, and netlist optimization. Contrary to other methods, the approach is based on a graph model of a circuit's clause description called implication graph. It combines both the flexibility of SAT-based techniques and high efficiency of structure based methods. As the proposed algorithms operate only on the implication graph, they are independent of the chosen logic. Evaluation of implications and computation of indirect implications are performed by simple and efficient graph algorithms. Experimental results for various applications relying on implication demonstrate the effectiveness of the approach.Keywords
This publication has 23 references indexed in Scilit:
- VERILAT: verification using logic augmentation and transformationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Functional learning: a new approach to learning in digital circuitsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Static logic implication with application to redundancy identificationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- AQUILA: An equivalence verifier for large sequential circuitsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Combinational test generation using satisfiabilityIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1996
- A transitive closure algorithm for test generationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1993
- Accelerated dynamic learning for test pattern generation in combinational circuitsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1993
- Test pattern generation using Boolean satisfiabilityIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1992
- Improved deterministic test pattern generation with applications to redundancy identificationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1989
- SOCRATES: a highly efficient automatic test pattern generation systemIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1988