Comparision between LPSAT and SMT for RTL verification

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.