This Article 
 Bibliographic References 
 Add to: 
Property Learning Techniques for Efficient Generation of Directed Tests
June 2011 (vol. 60 no. 6)
pp. 852-864
Mingsong Chen, East China Normal University, Shanghai
Prabhat Mishra, University of Florida, Gainesville
Property falsification in model checking is widely used for automated generation of directed tests. Due to state space explosion problem, traditional model checking techniques cannot handle large scale designs. SAT-based bounded model checking is promising to address the prohibitively large time and resource requirements during the property falsification. This article presents several efficient learning techniques that can improve the overall test generation time for a single property as well as a cluster of similar properties. The goal is to exploit both variable assignments and common conflict clauses of the prechecked partial or similar SAT instances for property falsification. Our method makes three novel contributions: 1) investigates the decision ordering-based learnings for a single SAT instance; 2) applies the decision ordering learnings between similar SAT instances; and 3) exploits the relation between the decision ordering-based learning and conflict clauses-based learning. Our experimental results using both software and hardware benchmarks demonstrate that our approach can drastically reduce the overall test generation time.

[1] J.W. Duran and S.C. Ntafos, "An Evaluation of Random Testing," IEEE Trans. Software Eng., vol. 10, no. 4, pp. 438-444, Apr. 1999.
[2] S. Fine and A. Ziv, "Coverage Directed Test Generation for Functional Verification Using Bayesian Networks," Proc. Design Automation Conf., pp. 286-291, 2003.
[3] A. Biere, A. Cimatti, E.M. Clarke, O. Strichman, and Y. Zhu, "Bounded Model Checking," Advances in Computers, vol. 58, no. 3, pp. 118-149, 2003.
[4] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, "Symbolic Model Checking Without BDDs," Proc. Fifth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 193-207, 1999.
[5] P.E. Ammann, P.E. Black, and W. Majurski, "Using Model Checking to Generate Tests from Specifications," Proc. Int'l Conf. Formal Eng. Methods, pp. 46-55, 1998.
[6] E. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 1999.
[7] J.E. Hopcroft, R. Motwani, and J.D. Ullman, Introduction to Automata Theory, Languages, and Computation, third ed. Addison-Wesley, 2006.
[8] A. Biere, A. Cimatti, E.M. Clarke, M. Fujita, and Y. Zhu, "Symbolic Model Checking Using SAT Procedures Instead of BDDs," Proc. Design Automation Conf., pp. 317-320, 1999.
[9] N. Amla, X. Du, A. Kuehlmann, R. Kurshan, and K. McMillan, "An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment," Proc. Correct Hardware Design and Verification Methods, vol. 3725, pp. 254-268, 2005.
[10] H. Koo and P. Mishra, "Test Generation Suing SAT-Based Bounded Model Checking for Validation of Pipelined Processors," Proc. Great Lake Symp. VLSI, pp. 362-365, 2006.
[11] H. Zhang, "SATO: An Efficient Propositional Prover," Proc. 14th Int'l Conf. Automated Deduction, pp. 272-275, 1997.
[12] M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, and S. Malik, "Chaff: Engineering an Efficient SAT Solver," Proc. 38th Design Automation Conf., pp. 530-535, 2001.
[13] J. Marques-Silva and K. Sakallah, "Grasp: A Search Algorithm for Propositional Satisfiability," IEEE Trans. Computers, vol. 48, no. 5, pp. 506-521, May 1999.
[14] I. Lynce and J. Marques-Silva, "Efficient Data Structures for Backtrack Search SAT Solvers," Annals of Math. and Artificial Intelligence, vol. 43, no. 1, pp. 137-152, 2005.
[15] V. Durairaj and P. Kalla, "Guiding CNF-SAT Search via Efficient Constraint Partitioning," Proc. Int'l Conf. Computer-Aided Design, pp. 498-501, 2004.
[16] V. Durairaj and P. Kalla, "Variable Ordering for Efficient SAT Search by Analyzing Constraint-Variable Dependencies," Proc. Int'l Conf. Theory and Applications of Satisfiability Testing, pp. 415-422, 2005.
[17] L. Zhang, C.F. Madigan, M.H. Moskewicz, and S. Malik, "Efficient Conflict Driven Learning in a Boolean Satisfiability Solver," Proc. Int'l Conf. Computer-Aided Design, pp. 279-285, 2001.
[18] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulations," IEEE Trans. Computers, vol. 35, no. 8, pp. 677-691, Aug. 1986.
[19] E.M. Clarke, O. Grumberg, and D.E. Long, "Model Checking and Abstraction," ACM Trans. Programming Languages and Systems, vol. 16, no. 5, pp. 1512-1542, 1994.
[20] P. Bjesse and J. Kukula, "Using Counter Example Guided Abstraction Refinement to Find Complex Bugs," Proc. Conf. Design, Automation, and Test in Europe, pp. 156-161, 2004.
[21] H. Koo and P. Mishra, "Functional Test Generation Using Design and Property Decomposition Techniques," ACM Trans. Embedded Computing Systems, vol. 8, no. 4, Article 32, July 2009.
[22] H. Jin and F. Somenzi, "An Incremental Algorithm to Check Satisfiability for Bounded Model Checking," Proc. Int'l Workshop Bounded Model Checking (BMC '04), vol. 119, no. 2, pp. 51-65, 2005.
[23] O. Strichman, "Pruning Techniques for the SAT-Based Bounded Model Checking Problem," Proc. 11th IFIP WG 10.5 Advanced Research Working Conf. Correct Hardware Design and Verification Methods, vol. 2144, pp. 58-70, 2001.
[24] M. Chen and P. Mishra, "Functional Test Generation Using Efficient Property Clustering and Learning Techniques," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 29, no. 3, pp. 396-404, Mar. 2010.
[25] M. Chen, X. Qiu, W. Xu, L. Wang, J. Zhao, and X. Li, "UML Activity Diagram Based Automatic Test Case Generation for Java Programs," The Computer J., vol. 52, no. 5, pp. 545-556, 2009.
[26] M. Chen and P. Mishra, "Efficient Decision Ordering Techniques for SAT-Based Test Generation," Proc. Conf. Design, Automation and Test in Europe, pp. 490-495, 2010.
[27] L. Zhang, M.R. Prasad, and M.S. Hsiao, "Incremental Deductive and Inductive Reasoning for SAT-Based Bounded Model Checking," Proc. IEEE/ACM Int'l Conf. Computer-Aided Design, pp. 502-509, 2004.
[28] P. Godefroid, N. Klarlund, and K. Sen, "DART: Directed Automated Random Testing," Proc. Conf. Programming Language Design and Implementation, pp. 213-223, 2005.
[29] K. Sen, D. Marinov, and G. Agha, "Cute: A Concolic Unit Testing Engine for C," Proc. Fifth Joint Meeting of the European Software Eng. Conf. and ACM SIGSOFT Symp. Foundations of Software Eng. (ESEC/FSE '05), pp. 263-272, 2005.
[30] D.A. Mathaikutty, S.K. Shukla, S.V. Kodakara, D. Lilja, and A. Dingankar, "Design Fault Directed Test Generation for Microprocessor Validation," Proc. Conf. Design, Automation and Test in Europe, pp. 761-766, 2007.
[31] J.P. Marques-Silva and K.A. Sakallah, "The Impact of Branching Heuristics in Propositional Satisfiability," Proc. Ninth Portuguese Conf. Artificial Intelligence, pp. 62-74, 1999.
[32] O. Shtrichman, "Tuning SAT Checkers for Bounded Model Checking," Proc. 12th Int'l Conf. Computer Aided Verification, pp. 480-494, 2000.
[33] C. Wang, H. Jin, G.D. Hachtel, and F. Somenzi, "Refining the SAT Decision Ordering for Bounded Model Checking," Proc. Design Automation Conf., pp. 535-538, 2004.
[34] M.N. Velev, "Automatic Abstraction of Equations in a Logic of Equality," Proc. Analytic Tableaux and Related Methods (TABLEAUX), pp. 196-213, 2003.
[35] M. Davis, G. Logemann, and D.W. Loveland, "A Machine Program for Theorem-Proving," Comm. the ACM, vol. 5, no. 7, pp. 394-397, 1962.
[36] SAT Benchmark Problems, description.html, 2011.
[37] Miroslav Velev's SAT Benchmarks, http://www.miroslav-velev. comsat_benchmarks.html , 2011.
[38] J. Hennessy and D. Patterson, Computer Architecture: A Quantitative Approach. Morgan Kaufmann Publishers, 2003.
[39] zChaff, , 2011.
[40] NuSMV, http:/, 2011.

Index Terms:
Bounded model checking, directed test generation, conflict clause forwarding, decision ordering.
Mingsong Chen, Prabhat Mishra, "Property Learning Techniques for Efficient Generation of Directed Tests," IEEE Transactions on Computers, vol. 60, no. 6, pp. 852-864, June 2011, doi:10.1109/TC.2011.49
Usage of this product signifies your acceptance of the Terms of Use.