Conflict-Driven Learning in Test Pattern Generation

Abstract:

SAT-based automatic test pattern generation (ATPG) is built on a SAT-solver, which can be scalable is that it is able to take into account the information of high-level structure of formulas. Paper analyzes specific structure of circuit instances where correlations among signals have been established. This analysis is a heuristic learning method by earlier detecting assignment conflicts. Reconvergent fanout is a fundamental cause of the difficulty in testing generation, because they introduce dependencies in the values that can be assigned to nodes. 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.

• Periodical: Advanced Materials Research (Volumes 301-303)
• Pages: 1089-1092
• DOI: https://doi.org/10.4028/www.scientific.net/AMR.301-303.1089
• Online since: July 2011
• Authors: Xin Liu
• Keywords: Automatic Test Pattern Generation (ATPG), Binary Decision Diagrams (BDDs), Boolean Satisfiability (SAT), Conflict-Driven Learning, Conjunctive Normal Form (CNF)

References

[1] T. Larrabee. Test pattern generation using Boolean satisfiability. IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems, 1992, 11 (2): 4-15.

DOI: 10.1109/43.108614

[2] P. Stephan, R.K. Brayton, and A.L. Sangiovanni-Vincentelli. Combinational test generation using satisfiability. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 1996, 15 (9): 1167-1176.

DOI: 10.1109/43.536723

[3] J. Silva, K. Sakallah. GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions of Computers, 1999, 48(5): 506-521.

DOI: 10.1109/12.769433

[4] Liu X., Xiong Y.L. Enhancing SAT-Based Test Pattern Generation. Journal of Electronic Science and Technology of China, 2005, 3(2): 134: 139.

[5] E. Goldberg and Y. Novikov. Equivalence Checking of Dissimilar Circuits. International Workshop on Logic & Synthesis (IWLS'2003), Laguna Beach, California, USA, 2003(5): 28-30.

[6] E. Goldberg. Proving Unsatisfiability of CNFs locally . Journal of Automated Reasoning. vol 28: 417-434, (2002).

[7] A. Gupta, M. Ganai, C. Wang, et al. Learning from BDDs in SAT-based Bounded Model Checking [C]. 40th Design Automation Conference, Anaheim, CA, 2003. 6: 824-829.

DOI: 10.1145/775832.776040

[8] R.E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transaction. on Computer, 1986, 35 (8): 677-691.

DOI: 10.1109/tc.1986.1676819

[9] T. Kirkland and M. R. Mercer. A topological search algorithm for ATPG. 24th ACM/IEEE Design Automation Conference, Miami Beach, FL, 1987: 502-508.

DOI: 10.1145/37888.37963

[10] T. Lengauer and R.E. Tarjan. A fast algorithm for finding dominators in flow graph. ACM Trans. on Prog. Lang. and Systems, 1979, 1 (1): 121-141.

DOI: 10.1145/357062.357071

[11] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an Efficient SAT Solver. 38th Design Automation Conference, Las Vegas, Nevada, 2001: 530-535.

DOI: 10.1145/378239.379017

[12] J.P. Marques-Silva and K.A. Sakallah. Robust search algorithms for test pattern generation. IEEE Fault-Tolerance Computing Symposium, Seattle, WA, 1997: 152–161.

DOI: 10.1109/ftcs.1997.614088