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

V
VLSID
2003
16th International Conference on VLSI Design
Abstract - Formal Verification Using Bounded Model Checking: SAT versus Sequential ATPG Engines

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Daniel G. Saab Articles by Jacob A. Abraham Articles by Vivekananda M. Vedula

16th International Conference on VLSI Design

New Delhi, India

January 04-January 08

ISBN: 0-7695-1868-0

	ASCII Text	x
	Daniel G. Saab, Jacob A. Abraham, Vivekananda M. Vedula, "Formal Verification Using Bounded Model Checking: SAT versus Sequential ATPG Engines," VLSI Design, International Conference on, pp. 243, 16th International Conference on VLSI Design, 2003.

	BibTex	x
	@article{ 10.1109/ICVD.2003.1183144, author = {Daniel G. Saab and Jacob A. Abraham and Vivekananda M. Vedula}, title = {Formal Verification Using Bounded Model Checking: SAT versus Sequential ATPG Engines}, journal ={VLSI Design, International Conference on}, volume = {0}, year = {2003}, issn = {1063-9667}, pages = {243}, doi = {http://doi.ieeecomputersociety.org/10.1109/ICVD.2003.1183144}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - VLSI Design, International Conference on TI - Formal Verification Using Bounded Model Checking: SAT versus Sequential ATPG Engines SN - 1063-9667 SP EP A1 - Daniel G. Saab, A1 - Jacob A. Abraham, A1 - Vivekananda M. Vedula, PY - 2003 KW - null VL - 0 JA - VLSI Design, International Conference on ER -

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

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICVD.2003.1183144

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.

Citation:

Daniel G. Saab, Jacob A. Abraham, Vivekananda M. Vedula, "Formal Verification Using Bounded Model Checking: SAT versus Sequential ATPG Engines," vlsid, pp.243, 16th International Conference on VLSI Design, 2003

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.