Formal Verification Using Bounded Model Checking: SAT versus Sequential ATPG Engines

Daniel G. Saab; Jacob A. Abraham; Vivekananda M. Vedula

doi:10.1109/ICVD.2003.1183144

VLSI Design, International Conference on

Formal Verification Using Bounded Model Checking: SAT versus Sequential ATPG Engines

Year: 2003, Pages: 243

DOI Bookmark: 10.1109/ICVD.2003.1183144

Authors

Daniel G. Saab, Case Western Reserve University
Jacob A. Abraham, The University of Texas at Austin
Vivekananda M. Vedula, The University of Texas at Austin

Abstract

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.

Like what you’re reading?

Already a member?

Get this article FREE with a new membership!

Instance Generation for SAT-based ATPG
2007 IEEE Design and Diagnostics of Electronic Circuits and Systems
Reusing Learned Information in SAT-based ATPG
2007 20th International Conference on VLSI Design
Speeding up SAT-Based ATPG Using Dynamic Clause Activation
2009 Asian Test Symposium
On the Influence of Boolean Encodings in SAT-Based ATPG for Path Delay Faults
38th International Symposium on Multiple Valued Logic (ismvl 2008)
SAT and ATPG: Boolean engines for formal hardware verification
2002 IEEE/ACM International Conference on Computer Aided Design (ICCAD)
Improving Test Pattern Compactness in SAT-based ATPG
16th Asian Test Symposium (ATS 2007)
TG-PRO: A new model for SAT-based ATPG
2009 IEEE International High Level Design Validation and Test Workshop
A fast untestability proof for SAT-based ATPG
2009 12th International Symposium on Design and Diagnostics of Electronic Circuits & Systems
An Analysis of ATPG and SAT algorithms for Formal Verification
Sixth IEEE International High-Level Design Validation and Test Workshop
Incremental SAT Instance Generation for SAT-based ATPG
2008 11th IEEE Workshop on Design and Diagnostics of Electronic Circuits and Systems

Formal Verification Using Bounded Model Checking: SAT versus Sequential ATPG Engines

Authors

Abstract

Related Articles