Abstract
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 constraint logic programming (CLP) techniques 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.
This work is supported by the National Science Foundation of China (NSFC) under grant No. 60403048 and 60303013.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (2003)
Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic theorem proving for predicate abstraction refinement. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 457–461. Springer, Heidelberg (2004)
Ball, T., Rajamani, S.K.: Boolean programs: A model and process for software analysis. Technical Report 2000-14, Microsoft Research (February 2000)
Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL 2002: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 191–202. ACM Press, New York (2002)
Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic Predicate Abstraction of C Programs. In: ACM Conference on Programming Language Design and Implementation, pp. 203–213. ACM Press, New York (2001)
Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)
Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular Verification of Software Components in C. IEEE Transactions on Software Engineering 30(6), 388–402 (2004)
Clarke, E., Talupur, M., Wang, D.: SAT based predicate abstraction for hardware verification. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 78–92. Springer, Heidelberg (2004)
Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. Formal Methods in System Design (FMSD) 25(2-3), 105–127 (2004)
Clarke, E., Jain, H., Kroening, D.: Predicate Abstraction and Re-finement Techniques for Verifying Verilog. Technical report, Carnegie Mellon University, CMU-CS-04-139 (June 2004)
Clarke, E., Jain, H., Kroening, D.: Verification of SpecC using Predicate Abstraction. MEMOCODE (June 2004)
Jaffar, J., Maher, M.J.: Constraint logic programming: A Survey. The Journal of Logic Programming 19, 20, 503–582 (1994)
Ubar, R.: Test synthesis with alternative graphs. IEEE Design & Test of Computers 13(1), 48–57 (1996)
Tun, L.: Research on techniques of VLSI RT-Level automatic functional vectors generation [Ph.D. Thesis] National University of Defense Technology, ChangSha (2003)
Li, T., Guo, Y., Li, S.: Functional Vectors Generation for RT-Level Verilog Descriptions Based on Path Enumeration and Constraint Logic Programming. To appear Proceedings of 8th Euromicro Conference on Digital System Design, Porto, Portugal (August 2005)
Silva, J.M.: BLIF2CNF, sat.inesc-id.pt/~jpms/scripts/bin/blif2cnf
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of 39th Design Automation Conference (DAC 2001), Las Vegas (June 2001)
McMillan, K.: Applying SAT Methods in Unbounded Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 250–264. Springer, Heidelberg (2002)
Sun Microsystems. PicoJava technology (1999), http://www.sun.com/microelectronics/communitysource/picojava/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Li, T., Guo, Y., Li, S., Liu, G. (2005). Predicate Abstraction of RTL Verilog Descriptions Using Constraint Logic Programming. In: Peled, D.A., Tsay, YK. (eds) Automated Technology for Verification and Analysis. ATVA 2005. Lecture Notes in Computer Science, vol 3707. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562948_15
Download citation
DOI: https://doi.org/10.1007/11562948_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29209-8
Online ISBN: 978-3-540-31969-6
eBook Packages: Computer ScienceComputer Science (R0)