Predicate Abstraction of RT-Levei Verilog Using Symbolic Simulation and Constraint Logic Programming
Qu Wan · Chinese Journal of Computers · 2007
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 tech- niques,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.Ex- perimental results have showed the promising improvements on the performance of predicate ab- straction of hardware designs.