Title :
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
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;
Conference_Titel :
High-Level Design Validation and Test Workshop, 2001. Proceedings. Sixth IEEE International
Conference_Location :
Monterey, CA
Print_ISBN :
0-7695-1411-1
DOI :
10.1109/HLDVT.2001.972826
