基于符号模拟和约束逻辑编程的RTL级Verilog谓词抽象方法

Predicate Abstraction of RT-Levei Verilog Using Symbolic Simulation and Constraint Logic Programming

利用人工智能最新研究成果——约束逻辑编程对Verilog描述进行谓词抽象,并与目前基于SAT的方法进行了比较．首先通过符号模拟建立Verilog的形式化模型,然后结合要抽象的谓词,将谓词抽象问题转化为约束逻辑编程问题并进行求解．该方法的优点是在计算抽象系统时,不需要像基于SAT的方法那样将字级约束打散成位级约束,求解效率显著提高;提供了一个统一的框架用于描述各种约束．实验结果表明,与基于SAT的抽象技术相比,基于约束逻辑编程的抽象方法的求解速度有显著提高．

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.