Speeding up SAT-Based ATPG Using Dynamic Clause Activation

Abstract—SAT-based ATPG turned out to be a robust alternative to classical structural ATPG algorithms such as FAN. The number of unclassified faults can be significantly reduced using a SAT-based ATPG approach. In contrast to structural ATPG, SAT solvers work on a Boolean formula in Conjunctive Normal Form (CNF). This results in some disadvantages for SAT solvers when applied to ATPG, e.g. CNF transformation time and loss of structural knowledge. As a result, SAT-based ATPG algorithms are very robust for hard-to-test faults, but suffer from the overhead for easy-to-test faults. We propose the SAT technique Dynamic Clause Activation (DCA) in order to reduce the run time gap between structural and SAT-based ATPG algorithms and, at the same time, retain the high level of robustness. Using DCA, the SAT solver works on a partial formula of a logic circuit which is dynamically extended during the search process using structural knowledge. Furthermore, efficient dynamic learning techniqu...

• Type: Conference
• Year: 2009
• Where: ATS
• Authors: Stephan Eggersglüß, Daniel Tille, Rolf Drechsler
• Keywords: ATS 2009, Hardware, Sat Solver, SAT-based ATPG, SAT-based ATPG Algorithms