COMBINATIONAL TEST-GENERATION USING SATISFIABILITY

We present a robust, efficient algorithm for combinational test genera tion using a reduction to satisfiability (SAT), The algorithm, Test Ge neration Using Satisfiability (TEGUS), solves a simplified test set ch aracteristic equation using straightforward but powerful greedy heuris tics, ordering the variables using depth-first search and selecting a variable from the next unsatisfied clause at each branching point, For difficult faults, the computation of global implications is iterated, which finds more implications than previous approaches and subsumes s tructural heuristics such as unique sensitization. Without random test s or fault simulation, TEGUS completes on every fault in the ISCAS net works, demonstrating its robustness, and is ten times faster for those networks which have been completed by previous algorithms, Our implem entation of TEGUS can be used as a base line for comparing test genera tion algorithms; we present comparisons with 45 recently published alg orithms. TEGUS combines the advantages of the elegant organization of SAT-based algorithms with the efficiency of structural algorithms.