An Efficient SAT-Based Test Generation Algorithm with GPU Accelerator

摘要

This paper presents a novel framework comprises of a Propositional Satisfiability (SAT) encoder and solver. The framework responsible for generating and proving a simplified SAT-based formula of digital circuits for Automatic Test Pattern Generation (ATPG) proposes. The parallel algorithms introduced in this work are aimed at both combinational and sequential circuits and optimized on NVIDIA General-Purpose Graphics Processing Unit (GPGPU) paradigm. The SAT encoder presents an efficient method to apply the Boolean Constraint Propagation (BCP) on-the-fly while the generation is running on the GPU. The simplified formula is further proved for satisfiability using an improved parallel solver on GPU. The proposed encoder executes 93times faster compared to the sequential counterpart. The test generation algorithm using the GPU-accelerated framework delivers about 5.86 speedup on anaverage compared to the state-of-the-art Lingeling solver. Moreover, the SAT encoder reduced the run time for fault detection by 6.53 and 11.42% on anaverage when applied to the proposed and the conventional CUD@SAT solvers, respectively, offering promising related work for thefuture research.