LPSAT: A unified approach to RTL satisfiability

LPSAT is an LP-based comprehensive infrastructure designed to solve the satisfiability (SAT) problem for complex RTL designs containing both word-level arithmetic operators and bit-level Boolean logic. The presented technique uses a mixed integer linear program to model the constraints corresponding to both domains of the design. Our technique renders the constraint propagation between the two domains implicit to the MILP solver; thus enhancing the overall efficiency of the SAT framework. The experimental results are quite promising when compared with generic CNF-based and BDD-based SAT algorithms.