Incremental SAT Instance Generation for SAT-based ATPG

Due to ever increasing design sizes more efficient tools for automatic test pattern generation (ATPG) are needed. Recently ATPG based on Boolean satisfiability (SAT) has been shown to be a beneficial complement to traditional ATPG techniques. This paper makes two contributions. Firstly, we analyze the two steps SAT-based ATPG consists of with respect to their run time on industrial benchmarks. Secondly, exploiting these analysis results, we propose an incremental solving technique with the objective to speed up the entire classification process. An experimental evaluation of the proposed method shows a significant reduction of the overall run time of the SAT- based ATPG process.