ATPG Method And Application Of Digital Circuits Based On SAT

Automatic Test Pattern Generation (ATPG) problems plays very important rolein digital circuits test phase. It is a critical procedure to judge the reliability ofproduction and affects the cost of designing and producing. It is not only hard to solvethe large-scale ATPG problems, but also cannot to handle hard-to-detect problems forthe traditional methods.With in-depth research of the Boolean Satisfiability (SAT) problems and theemergence of efficient SAT solver, it is possible to solve the large-scale BooleanSatisfy (SAT) problems. This paper uses effectual methods to parse and abstract theintegrate circuits model which is descript by Verilog, and transform the gate-levelmodel to the Conjunctive Normal Form (CNF), then and build the model for theSingle Stuck-at Fault (SSF), by constructing the miter, translate the ATPG problemsinto SAT problems solved by the SAT-solver. Meanwhile, it also introduces theimplement process.It can be applied in Equivalence checking of integrate circuits by building anthermodel. Equivalence checking which affects the design circle of production is one ofthe most popular verification techniques in circuits design phase. This paperconstructs the miter to connect the reference circuit and implementation circuit, anddo elaborate the model descript by Verilog which is transformed to Static SingleAssignment (SSA) presentation, and solved by Satisfiability Modulo Theories (SMT).