Multi-targeting boolean satisfiability-based test pattern generation
View Patent ↗Disclosed are representative examples of methods, apparatus, and systems for generating test patterns targeting multiple faults using Boolean Satisfiability (SAT)-based test pattern generation methods. A SAT instance is constructed based on the circuit design information and a set of faults being targeted. A SAT solving engine is applied to the SAT instance to search for a test pattern for detecting the set of faults. The SAT instance or the SAT solving engine may be modified so that the SAT solving engine will search for a test pattern for detecting a maximum number of faults in the set of faults.
1. A method of multi-target Boolean Satisfiability (SAT)-based pattern generation, comprising:
receiving circuit design information for a circuit and a set of faults that model a plurality of potential defects in the circuit;
constructing a SAT instance based on the circuit design information and the set of faults;
applying a SAT solving engine to the SAT instance to derive a satisfying assignment; and
outputting a test pattern based on the satisfying assignment or a report that a test pattern cannot be generated.
2. The method recited in claim 1 , wherein the circuit design information comprises netlist information of the circuit.
3. The method recited in claim 1 , wherein the test pattern is capable of detecting a maximum number of faults in the set of faults.
4. The method recited in claim 1 , wherein the SAT solving engine is configured based on a pseudo-Boolean constraint, the pseudo-Boolean constraint causing the SAT solving engine to derive the satisfying assignment that is converted to the test pattern, the test pattern being capable of detecting a maximum number of faults in the set of faults.
5. The method recited in claim 1 , wherein the constructing a SAT instance comprises:
constructing an extended Milter structure derived based on the circuit design information and the set of faults; and
transforming the extended Milter structure to the SAT instance.
6. The method recited in claim 1 , wherein the constructing a SAT instance is further based on a pseudo-Boolean constraint, the pseudo-Boolean constraint maximizing causing the SAT solving engine to derive the satisfying assignment that is converted to the test pattern, the test pattern being capable of detecting a maximum number of faults in the set of faults.
7. The method recited in claim 1 , wherein the set of faults are derived after applying a different ATPG method to an original set of faults.
8. A non-transitory processor-readable medium storing processor-executable instructions for causing one or more processors to perform a method of multi-target Boolean Satisfiability (SAT)-based pattern generation, the method comprising:
receiving circuit design information for a circuit and a set of faults that model a plurality of potential defects in the circuit;
constructing a SAT instance based on the circuit design information and the set of faults;
applying a SAT solving engine to the SAT instance to derive a satisfying assignment; and
outputting a test pattern based on the satisfying assignment or a report that a test pattern cannot be generated.
9. The non-transitory processor-readable medium recited in claim 8 , wherein the circuit design information comprises netlist information of the circuit.
10. The non-transitory processor-readable medium recited in claim 8 , wherein the test pattern is capable of detecting a maximum number of faults in the set of faults.
11. The non-transitory processor-readable medium recited in claim 8 , wherein the SAT solving engine is configured based on a pseudo-Boolean constraint, the pseudo-Boolean constraint causing the SAT solving engine to derive the satisfying assignment that is converted to the test pattern, the test pattern being capable of detecting a maximum number of faults in the set of faults.
12. The non-transitory processor-readable medium recited in claim 8 , wherein the constructing a SAT instance comprises:
constructing an extended Milter structure derived based on the circuit design information and the set of faults; and
transforming the extended Milter structure to the SAT instance.
13. The non-transitory processor-readable medium recited in claim 8 , wherein the constructing a SAT instance is further based on a pseudo-Boolean constraint, the pseudo-Boolean constraint maximizing causing the SAT solving engine to derive the satisfying assignment that is converted to the test pattern, the test pattern being capable of detecting a maximum number of faults in the set of faults.
14. The non-transitory processor-readable medium recited in claim 8 , wherein the set of faults are derived after applying a different ATPG method to an original set of faults.