Formal verification using bounded model checking: SAT versus sequential ATPG engines

Industry is beginning to use Satisfiability (SAT) solvers extensively for formally verifying the correctness of digital designs. In this paper we compare the performance of SAT solvers with sequential Automatic Test Pattern Generation (ATPG) techniques for property verification. Our experimental results on the ISCAS benchmarks as well as a model of the 8085 microprocessor show that, contrary to popular belief, ATPG techniques perform much better than SAT based verification techniques, especially for large designs.