SAT-based Automatic Test Pattern Generation Of VLSI

As today's VLSI designs grow in scale and complexity, errors become more frequent and difficult to track in the design process of integrated circuits, so testing techniques for faults are more and more requested, one of which is Automatic Test Pattern Generation (ATPG). ATPG can generate automatically test vectors for specific faults using some algorithms such as D, path sensibilization or Boolean difference. This paper studies the ATPG algorithms which use satisfiability(SAT) solver as the search engine. The contents are outlined as following:First, the ATPG algorithm for single stuck-at faults of bincomational circuit is presented and implemented. We use a method similar to Boolean difference, i.e. construct a new circuit by XORing the faulty and fault-free circuits and translate the new circuit into a CNF which will be sent to a SAT solver for finding the test vectors.Second, using above algorithm, we get the set of test vectors for all faults in the circuit, which is called fault dictionary. The fault diagnosis tree can then be generated according to the fault dictionary to find easily the corresponding sets of the test vectors for specific faults in the circuit.Last, the ATPG techniques for path delay faults are studied. It exploits similar idea to that used for single stuck-at fault, but is based on 7-values logic system so the CNF generation process differs. The algorithm can generate test vectors for robust and non-robust testing.The above three algorithms is implemented in C and tested on a set of ISCAS circuits. The results obtained demonstrate the effectiveness and feasibility of the proposed algorithms.