On the Influence of Boolean Encodings in SAT-based ATPG for Path Delay Faults

Automatic Test Pattern Generation (ATPG) is an important task to ensure that a chip functions correctly. For high speed chips, testing for dynamic fault models such as the path delay fault model becomes more and more important. While classical algorithms for ATPG reach their limit, the significance of algorithms to solve the Boolean Satisfiability (SAT) problem grows due to recent developments of powerful SAT solvers. However, ATPG is not always a purely Boolean problem. For generating robust test patterns for delay faults, multiple-valued logics are needed. To apply a (Boolean) SAT solver on a problem modeled in multiple-valued logic, a Boolean encoding has to be used. In this paper, we consider the problem of SAT-based ATPG for the robust path delay fault model where a 19-valued logic is used and provide a detailed study on the influence of the chosen Boolean encoding on the performance of test generation. Further, we show a method to identify efficient encodings and show the behavior of these encodings on ISCAS benchmarks and large industrial circuits.