Incremental Solving Techniques for SAT-based ATPG

Automatic test pattern generation (ATPG) based on the Boolean satisfiability (SAT) problem has recently been proven to be a beneficial complement to traditional methods. Efficient SAT techniques yield a robust fault classification. In this paper, we present methodologies to improve the efficiency of SAT-based ATPG. First, we give a detailed run time analysis of a state-of-the-art SAT-based ATPG tool. By only taking circuit partitions into account and applying incremental SAT solving, both SAT instance generation and SAT instance solving can be accelerated and the robustness of the ATPG process is increased. Besides the significant run time reduction of SAT-based ATPG, the methodology can additionally be used to improve the test set quality. The proposed techniques are applied for the stuck-at and for the transition fault model. A set of large industrial designs is used to show the efficiency of the approach.