Comparision between LPSAT and SMT for RTL verification

Author

Kunapareddy, Sarvani ; Turaga, Sriraj Dheeraj ; Sajjan, Solomon Surya Tej Mano

Author_Institution

Electr. & Comput. Eng., Univ. of Utah, Salt Lake City, UT, USA

fYear

2015

fDate

19-20 March 2015

Firstpage

1

Lastpage

5

Abstract

The complexity of the circuits today are making it impossible to verify those using traditional CNF-based and BDD-based SAT algorithms. They take unacceptably long run times. Circuits are so complex that bit blasting them is infeasible. A better solution to this problem is to solve SAT at word level. LP solvers and SMT solvers are more efficient to tackle such high complexity at word level. The world today has moved to SMT solvers in verification of world level RTL. Our study aims at the comparison between LP solvers and SMT solvers in verification of RTL. This comparison is made on the basis of complexity, number of iterations and run time. SMT is found to complete verification check in less number of iterations and time. It also has less code complexity and is easy to understand.

Keywords

circuit complexity; computability; iterative methods; linear programming; program verification; BDD-based SAT algorithms; CNF-based SAT algorithms; LP solvers; RTL verification; SMT solvers; circuit complexity; code complexity; conjunctive normal form; iteration number; linear programming; verification check; word level satisfiability; Boolean functions; Complexity theory; Computers; Data structures; Hardware design languages; Integrated circuit modeling; Logic gates; Bit nibbling; CNF; LPSAT; RTL Verification; SMT; Satisfiability;

fLanguage

English

Publisher

ieee

Conference_Titel

Circuit, Power and Computing Technologies (ICCPCT), 2015 International Conference on

Conference_Location

Nagercoil

Type

conf

DOI

10.1109/ICCPCT.2015.7159418

Filename

7159418