Improving Test Pattern Generation with Implication Learning

Nowadays SAT algorithms allow 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 by analyzing specific structure of circuit instances. This analysis is called heuristic learning where correlations among signals have been established by simple and efficient methods. It is achieved by finding more necessary signal line assignments, by detecting conflicts earlier, and by 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 clauses to restrict and focus the overall search space of test pattern generation. The experimental results demonstrate the effectiveness of these learning techniques.