Formal verification using bounded model checking: SAT versus sequential ATPG engines

Author

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

Author_Institution

Dept. of Electr. Eng. & Comput. Sci., Case Western Reserve Univ., Cleveland, OH, USA

fYear

2003

fDate

4-8 Jan. 2003

Firstpage

243

Lastpage

248

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.

Keywords

automatic test pattern generation; circuit CAD; computability; formal verification; integrated circuit design; logic CAD; sequential circuits; 8085 microprocessor model; ISCAS benchmarks; SAT based verification; bounded model checking; formal verification; satisfiability solvers; sequential ATPG engines; sequential automatic test pattern generation; Automatic test pattern generation; Boolean functions; Computer bugs; Data structures; Design engineering; Engines; Formal verification; Jacobian matrices; Logic design; Testing;

fLanguage

English

Publisher

ieee

Conference_Titel

VLSI Design, 2003. Proceedings. 16th International Conference on

ISSN

1063-9667

Print_ISBN

0-7695-1868-0

Type

conf

DOI

10.1109/ICVD.2003.1183144

Filename

1183144