Predicate abstraction of RT-Level Verilog using symbolic simulation and constraint logic programming

Abstraction is one of the most effective ways to address state explosion problem in model checking, and predicate abstraction has been applied successfully to large software and now to hardware descriptions, such as Verilog. This paper evaluates the state-of-the-art AI techniques, constraint logic programming (CLP), to improve the performance of predicate abstraction of circuits, and compared it with the SAT-based predicate abstraction techniques. With CLP-based techniques, we can model various constraints in a unified framework; we can also model the word-level constraints without flattening them into bit-level ones as SAT-based method dose. Experimental results have showed the promising improvements on the performance of predicate abstraction of hardware designs.