Improving CNF representations in SAT-based ATPG for industrial circuits using BDDs

It was shown in the past that ATPG based on the Boolean Satisfiability problem is a beneficial complement to traditional ATPG techniques. Its advantages can be observed especially on large industrial circuits. These circuits usually contain a lot of functional redundancy which, on the one hand, is often needed during operational mode, but on the other hand, causes dispensable overhead during ATPG. Using the traditional circuit-to-CNF transformation, this redundancy is also contained in the SAT instances. The contribution of this paper is a new technique to improve the SAT instance generation for SAT-based ATPG. The objective of the proposed method is to use Binary Decision Diagrams (BDDs) to optimize the resulting CNF representations. In order to apply the proposed technique to industrial circuits, we developed dedicated BDD operations using a multiple-valued logic. The experimental results, obtained on large industrial designs, show that the accomplished optimizations result in a considerable acceleration of the overall ATPG runtime as well as in a significant reduction of the unclassified faults.