A major technique to address state explosion problem in model checking is abstraction. 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 predication abstraction of hardware designs, and compared it with the SAT-based predicate abstraction techniques. With CLP based techniques, we can model various constraints, such as bit, bit-vector and integer, in a uniform framework; we can also model the word-level constraints without flatting them into bit-level constraints as SAT-based method does. With these advantages, the computation of abstraction system can be more efficient than SAT-based techniques. We have implemented this method, and the experimental results have shown the promising improvements on the performance of predicate abstraction of hardware designs. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Li, T., Guo, Y., Li, S. K., & Zhu, D. (2005). Applying constraint logic programming to predicate abstraction of RTL Verilog descriptions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3789 LNAI, pp. 175–184). Springer Verlag. https://doi.org/10.1007/11579427_18
Mendeley helps you to discover research relevant for your work.