An analysis of ATPG and SAT algorithms for formal verification

Author

Parthasarathy, G. ; Huang, Chung-Yang ; Cheng, Kwang-Ting

Author_Institution

California Univ., Santa Barbara, CA, USA

fYear

2001

fDate

2001

Firstpage

177

Lastpage

182

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

Keywords

Boolean algebra; automatic test pattern generation; computability; formal verification; logic CAD; Automatic Test Pattern Generation algorithms; breadth-first decision orderings; depth-first decision orderings; hardware verification; satisfiability; state-of-the-art solvers; Algorithm design and analysis; Automatic test pattern generation; Boolean functions; Data structures; Flexible printed circuits; Formal verification; Hardware; Logic testing; Performance analysis; Search engines;

fLanguage

English

Publisher

ieee

Conference_Titel

High-Level Design Validation and Test Workshop, 2001. Proceedings. Sixth IEEE International

Conference_Location

Monterey, CA

Print_ISBN

0-7695-1411-1

Type

conf

DOI

10.1109/HLDVT.2001.972826

Filename

972826