Advanced utilization of formal methods in automatic test pattern generation for industrial designs

The focus of this thesis is to improve SAT-based ATPG by addressing the shortcomings listed above. Several new techniques are proposed to expand the first promising results on academical benchmarks to large industrial designs. The contributions include several methodologies that • improve performance significantly, • increase the overall robustness, and • enable the application in an industrial framework. The developed techniques target ATPG for the widely distributed stuck-at fault model as well as for the more complex transition fault model. This thesis consists of three parts. The first part introduces the preliminaries. Basic definitions are given and related work is reported. The second part proposes several techniques to optimize SAT instances derived from the circuit-oriented ATPG problem. A CNF generation that extracts the problem from a circuit has a central disadvantage: every circuit information that is actually unnecessary during ATPG is also contained in the SAT instance. Examples are redundancy that is contained in the circuit and “uninteresting” circuit parts. This “blows up” the CNF. In general, the complexity of solving a SAT instance correlates with its size; the more variables and clauses a CNF contains, the more run time is required by a SAT solver. The proposed methods target the instance generation process to obtain optimized CNFs. This improves performance as well as robustness. The third part concentrates on the application in an industrial environment. A central drawback of SAT-based ATPG is the loss of circuit information. Classical ATPG algorithms applied in industrial practice, on the other hand, operate directly on the circuit structure and therefore profit from knowledge about the circuit during their search. The contribution of this part is the application of industrial techniques to SAT-based ATPG. The methodologies proposed in this thesis were implemented and integrated as a prototype into the ATPG framework of NXP Semiconductors. Furthermore, they are evaluated using large industrial designs containing up to 3.8 millions of elements.