Chinese Journal of Computers   Full Text
Title	Predicate Abstraction of RT-Level Verilog Using Symbolic Simulation and Constraint Logic Programming
Authors	LI Tun QU Wan-Xia GUO Yang LIU Gong-Jie LI Si-Kun
Address	(School of Computer Science & Technology, National University of Defense Technology, Changsha 410073)
Year	2007
Issue	No.7(1138—1144)
Abstract &   Background	Abstract 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. keywords predicate abstraction; Verilog constraint logic programming; model checking; symbolic simulation background Predicate abstraction is a powerful technique for addressing state explosion problem in model checking. Theorem prover is the first solver for computing abstract model, and now more and more attention is paid to predicate abstraction based on SAT. However, there are some limitations when using theorem prover and SAT for predicate abstraction. Firstly, theorem prover based method has to call the theorem prover many times during abstraction, which will make the abstraction process inefficient. Secondly, theorem provers model the variables using unbounded integer numbers. Overflow or bit-wise operators are not modeled. However, hardware description languages like Verilog provide an extensive set of bit-wise operators. Thirdly, although SAT based method can only call the SAT solver one time during abstraction, it has to flatten the word-level constraints into bit-level constraints, which will lose most of the word-level information and the runtime of this process typically grows exponentially with the number of predicates. This paper focuses on applying constraint logic programming (CLP) to predication abstraction of RTL Verilog descriptions, especially using CLP to solve the abstraction computation constraints obtained from circuit model and predicates. CLP-based method can model bit, bit-vector and bounded integer in a uniform framework, and can support various arithmetic and logic operations. What’s more, the word-level constraints are solved with word-level information and without flattening them into bit-level constraints. Owing to the expressiveness of logic programming and the constraints solving techniques, CLP-based method bridges the gap between EDA research and the research progress in constraint satisfaction problem and artificial intelligence area. This work is supported by the National Science Foundation of China (NSFC) under Grant No.60403048 and No.60573173, which focus on SOC system-level function verification and coverage-driven functional verification. Researchers from the two groups have an in-depth study in ASIC design and verification, parallel test generation and VLSI simulation vector generation domains. They have taken part in the design and verification in some microprocessors and ASIC chips during the last few years and obtained a series of significant results in theory, algorithm, design method and environment. Research on coverage-driven VLSI functional verification and SOC system-level functional verification will speedup SOC design verification progress and improve the quality of SOC design, which is very important to promote the design and verification abilities of integrated circuit in China.