Dynamic Compaction using Multi-Valued Encoding in SAT-based ATPG

SAT solvers have been at the forefront of ATPG solutions due to the inherent advantages of transforming the circuit to a mathematical problem. One that can quickly be solved by tried and true algorithms, rather than using traditional circuit based solutions. Unfortunately while this speedup may find a test vector for a specific fault to be detected, the number of test vectors detected for the entire fault list is usually very large due to this being a circuit structure. We present a system for dynamically compacting the test vector set as it searches for individual vectors, hence giving out fewer patterns that cover more faults. Three-valued encoding was used to allow the use of don't cares, a value that is not part of the traditional SAT solver approach. Experimental results compare the traditional approach with that of this new system's results.