Speeding-up test pattern generation by means of heuristic learning

Boolean Satisfiability (SAT) algorithms have seen dramatic improvements over recent years, allowing larger problem instances to be solved in application domains such as automatic test pattern generation (ATPG) that can also be viewed as solving a SAT problem. The key to a SAT-solver can be scalable is that it is able to take into account the information of high-level structure of formulas. This paper further improves to SAT-based ATPG with heuristic learning. It establishes correlations among signals by analyzing specific structure of circuit instances, finding more necessary signal line assignments, detecting conflicts earlier, and avoiding unnecessary work during test generation. Among others things, it combines strengths of binary decision graphs (BDD) and SAT techniques to improve the efficiency of test generation. Reconvergent fanout is a fundamental cause of the difficulty in testing circuits, because they introduce dependencies in the values that can be assigned to nodes. This paper exploits reconvergent fanout analysis of circuit to gather information about local signal correlation through BDD learning, and then used the learned information in the conjunctive normal form (CNF) clauses to restrict and focus the overall search space of test pattern generation. The experimental results demonstrate the effectiveness of these learning techniques.