An analysis of ATPG and SAT algorithms for formal verification

G. Parthasarathy; Chung Yang Huang; Kwang Ting Cheng

doi:10.1109/HLDVT.2001.972826

An analysis of ATPG and SAT algorithms for formal verification

G. Parthasarathy, Chung Yang Huang, Kwang Ting Cheng

Research output: Chapter in Book/Conference Proceeding/Report › Conference Paper published in a book › peer-review

19 Citations (Scopus)

Abstract

We analyze the performance of satisfiability (SAT) and Automatic Test Pattern Generation (ATPG) algorithms in two state-of-the-art solvers. The goal is to best understand how features of each solver are suited for hardware verification. For ATPG, we analyze depth-first and breadth-first decision orderings and effects of two weighting heuristics in the decision ordering, and also study the effect of randomization of decisions. Features of ATPG and SAT that affect their robustness and flexibility on real circuits are studied, and the two solvers are compared on 24 industrial circuits. We further analyze the results to identify the strengths and shortcomings of each solver. This will enable incorporation of features from each solver in order to optimize performance, since they both operate on the same principles.

Original language	English
Title of host publication	Proceedings - 6th IEEE International High-Level Design Validation and Test Workshop, HLDVT 2002
Publisher	IEEE Computer Society
Pages	177-182
Number of pages	6
ISBN (Electronic)	0769514111
DOIs	https://doi.org/10.1109/HLDVT.2001.972826
Publication status	Published - 2001
Externally published	Yes
Event	6th IEEE International High-Level Design Validation and Test Workshop, HLDVT 2002 - Monterey, United States Duration: 7 Nov 2001 → 9 Nov 2001

Publication series

Name	Proceedings - IEEE International High-Level Design Validation and Test Workshop, HLDVT
Volume	2001-January
ISSN (Print)	1552-6674

Conference

Conference	6th IEEE International High-Level Design Validation and Test Workshop, HLDVT 2002
Country/Territory	United States
City	Monterey
Period	7/11/01 → 9/11/01

Bibliographical note

Publisher Copyright:
© 2001 IEEE.

Access to Document

10.1109/HLDVT.2001.972826

Cite this

Parthasarathy, G., Huang, C. Y., & Cheng, K. T. (2001). An analysis of ATPG and SAT algorithms for formal verification. In Proceedings - 6th IEEE International High-Level Design Validation and Test Workshop, HLDVT 2002 (pp. 177-182). Article 972826 (Proceedings - IEEE International High-Level Design Validation and Test Workshop, HLDVT; Vol. 2001-January). IEEE Computer Society. https://doi.org/10.1109/HLDVT.2001.972826

@inproceedings{657baf7c0d7a411e8fedf0b5a76a92a4,

title = "An analysis of ATPG and SAT algorithms for formal verification",

abstract = "We analyze the performance of satisfiability (SAT) and Automatic Test Pattern Generation (ATPG) algorithms in two state-of-the-art solvers. The goal is to best understand how features of each solver are suited for hardware verification. For ATPG, we analyze depth-first and breadth-first decision orderings and effects of two weighting heuristics in the decision ordering, and also study the effect of randomization of decisions. Features of ATPG and SAT that affect their robustness and flexibility on real circuits are studied, and the two solvers are compared on 24 industrial circuits. We further analyze the results to identify the strengths and shortcomings of each solver. This will enable incorporation of features from each solver in order to optimize performance, since they both operate on the same principles.",

author = "G. Parthasarathy and Huang, \{Chung Yang\} and Cheng, \{Kwang Ting\}",

note = "Publisher Copyright: {\textcopyright} 2001 IEEE.; 6th IEEE International High-Level Design Validation and Test Workshop, HLDVT 2002 ; Conference date: 07-11-2001 Through 09-11-2001",

year = "2001",

doi = "10.1109/HLDVT.2001.972826",

language = "English",

series = "Proceedings - IEEE International High-Level Design Validation and Test Workshop, HLDVT",

publisher = "IEEE Computer Society",

pages = "177--182",

booktitle = "Proceedings - 6th IEEE International High-Level Design Validation and Test Workshop, HLDVT 2002",

}

Parthasarathy, G, Huang, CY & Cheng, KT 2001, An analysis of ATPG and SAT algorithms for formal verification. in Proceedings - 6th IEEE International High-Level Design Validation and Test Workshop, HLDVT 2002., 972826, Proceedings - IEEE International High-Level Design Validation and Test Workshop, HLDVT, vol. 2001-January, IEEE Computer Society, pp. 177-182, 6th IEEE International High-Level Design Validation and Test Workshop, HLDVT 2002, Monterey, United States, 7/11/01. https://doi.org/10.1109/HLDVT.2001.972826

An analysis of ATPG and SAT algorithms for formal verification. / Parthasarathy, G.; Huang, Chung Yang; Cheng, Kwang Ting.
Proceedings - 6th IEEE International High-Level Design Validation and Test Workshop, HLDVT 2002. IEEE Computer Society, 2001. p. 177-182 972826 (Proceedings - IEEE International High-Level Design Validation and Test Workshop, HLDVT; Vol. 2001-January).

Research output: Chapter in Book/Conference Proceeding/Report › Conference Paper published in a book › peer-review

TY - GEN

T1 - An analysis of ATPG and SAT algorithms for formal verification

AU - Parthasarathy, G.

AU - Huang, Chung Yang

AU - Cheng, Kwang Ting

PY - 2001

Y1 - 2001

N2 - We analyze the performance of satisfiability (SAT) and Automatic Test Pattern Generation (ATPG) algorithms in two state-of-the-art solvers. The goal is to best understand how features of each solver are suited for hardware verification. For ATPG, we analyze depth-first and breadth-first decision orderings and effects of two weighting heuristics in the decision ordering, and also study the effect of randomization of decisions. Features of ATPG and SAT that affect their robustness and flexibility on real circuits are studied, and the two solvers are compared on 24 industrial circuits. We further analyze the results to identify the strengths and shortcomings of each solver. This will enable incorporation of features from each solver in order to optimize performance, since they both operate on the same principles.

AB - We analyze the performance of satisfiability (SAT) and Automatic Test Pattern Generation (ATPG) algorithms in two state-of-the-art solvers. The goal is to best understand how features of each solver are suited for hardware verification. For ATPG, we analyze depth-first and breadth-first decision orderings and effects of two weighting heuristics in the decision ordering, and also study the effect of randomization of decisions. Features of ATPG and SAT that affect their robustness and flexibility on real circuits are studied, and the two solvers are compared on 24 industrial circuits. We further analyze the results to identify the strengths and shortcomings of each solver. This will enable incorporation of features from each solver in order to optimize performance, since they both operate on the same principles.

UR - https://www.webofscience.com/wos/woscc/full-record/WOS:000173394000028

UR - https://openalex.org/W1838320025

UR - https://www.scopus.com/pages/publications/0346868422

U2 - 10.1109/HLDVT.2001.972826

DO - 10.1109/HLDVT.2001.972826

M3 - Conference Paper published in a book

T3 - Proceedings - IEEE International High-Level Design Validation and Test Workshop, HLDVT

SP - 177

EP - 182

BT - Proceedings - 6th IEEE International High-Level Design Validation and Test Workshop, HLDVT 2002

PB - IEEE Computer Society

T2 - 6th IEEE International High-Level Design Validation and Test Workshop, HLDVT 2002

Y2 - 7 November 2001 through 9 November 2001

ER -

Parthasarathy G, Huang CY, Cheng KT. An analysis of ATPG and SAT algorithms for formal verification. In Proceedings - 6th IEEE International High-Level Design Validation and Test Workshop, HLDVT 2002. IEEE Computer Society. 2001. p. 177-182. 972826. (Proceedings - IEEE International High-Level Design Validation and Test Workshop, HLDVT). doi: 10.1109/HLDVT.2001.972826

An analysis of ATPG and SAT algorithms for formal verification

Abstract

Publication series

Conference

Bibliographical note

Access to Document

Other files and links

Fingerprint

Cite this