Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Learning-oriented Property Decomposition for Automated Generation of Directed Tests

  • Published:
Journal of Electronic Testing Aims and scope Submit manuscript

Abstract

SAT-based Bounded Model Checking (BMC) is promising for automated generation of directed tests. Due to the state space explosion problem, SAT-based BMC is unsuitable to handle complex properties with large SAT instances or large bounds. In this paper, we propose a framework to automatically scale down the SAT falsification complexity by utilizing the decision ordering based learning from decomposed sub-properties. Our framework makes three important contributions: i) it proposes learning-oriented decomposition techniques for complex property falsification, ii) it proposes an efficient approach to accelerate the complex property falsification using the learning from decomposed sub-properties, and iii) it combines the advantages of both property decomposition and property clustering to reduce the overall test generation time. The experimental results using both software and hardware benchmarks demonstrate the effectiveness of our framework.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13

Similar content being viewed by others

Notes

  1. In this paper, v=1, v=0 and v=X indicate that the Boolean variable v equals to true, false and UNKNOWN respectively.

  2. Here, COI indicates the variables involved during the property checking.

  3. A k-interaction property involves interactions among k components. For example, “!F(decode.stall ∼=1 & fetch.stall ∼=1) ″ is a 2-interaction property that involves interactions between fetch and decode units.

References

  1. Amla N, Du X, Kuehlmann A, Kurshan R, McMillan K (2005) An analysis of SAT-based model checking techniques in an industrial environment. Proceedings of Correct Hardware Design and Verification Methods (CHARME): 254–268

  2. Amla N, Emerson EA, Namjoshi KS (1999) Efficient decompositional model checking for regular timing diagrams. Proc Correct Hardware Des Verification Methods (CHARME): 67– 81

  3. Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. Proc Tools Algorithme Constr Anal Syst (TACAS): 193–207

  4. Bjesse P, Kukula JH (2004) Using counter example guided abstraction refinement to find complex bugs. Proc Des, Autom, Test Europe (DATE): 156–161

  5. Chang K, Bertacco V, Markov IL (2007) Simulation-based bug trace minimization with BMC-based refinement. IEEE Trans CAD Integr Circ Syst (TCAD) 26(1):152–165

    Article  Google Scholar 

  6. Chen M, Mishra P (2010) Functional test generation using efficient property clustering and learning techniques. IEEE Trans Comput-Aided Des Integr Circ Syst (TCAD) 29 (3): 396–404

    Article  Google Scholar 

  7. Chen M, Mishra P (2011) Decision ordering based property decomposition for functional test generation. Proc Des, Autom Test Europe (DATE): 167–172

  8. Li A, Chen M (2012) Efficient self-learning techniques for SAT-based test generation. Proc Int Conf Hardware/Software Codesign Syst Synth (CODES+ISSS): 197–206

  9. Chen M, Mishra P (2011) Property learning techniques for efficient generation of directed tests. IEEE Trans Comput 60 (6): 852–864

    Article  MathSciNet  Google Scholar 

  10. Mishra P, Dutt N (2004) Graph-based functional test program generation for pipelined processors. Proc Des, Autom Test Europe (DATE): 182–187

  11. Chen M, Qin X, Koo H, Mishra P (2012) System-Level Validation: High-Level Modeling and Directed Test Generation Techniques. Springer

  12. Clarke E, Grumberg O, Peled D (1999) Model Checking. MIT Press

  13. Dijkstra EW (1959) A note on two problems in connexion with graphs. Numerische Mathematik 1:269–271

    Article  MATH  MathSciNet  Google Scholar 

  14. Durairaj V, Kalla P (2005) Variable ordering for efficient SAT search by analyzing constraint-variable dependencies. Proc Int Conf Theory Appl Satisfiability Test (SAT): 415–422

  15. Eén N, Sörensson N (2003) An extensible SAT-solver. Proc Theory Appl Satisfiability (SAT): 502–518

  16. Eggersglüß S, Drechsler R (2011) Efficient data structures and methodologies for SAT-Based ATPG providing high fault coverage in industrial application. IEEE Trans CAD Integr Circ Syst (TCAD) 30(9):1411–1415

    Article  Google Scholar 

  17. Harris IG (2003) Fault models and test generation for hardware-software covalidation. IEEE Des Test 20(4):40–47

    Article  Google Scholar 

  18. Jin H, Somenzi F (2004) An incremental algorithm to check satisfiability for bounded model checking. Proc Int Work Bounded Model Checking: 51–65

  19. Koo H, Mishra P (2009). ACM Trans Embed Comput Syst (TECS) 8 (4)

  20. Mishra P, Shrivastava A, Dutt N (2006) Architecture description language (ADL)-driven software toolkit generation for architectural exploration of programmable SOCs. ACM Trans Des Autom Electron Syst (TODAES) 11(3):626–658

    Article  Google Scholar 

  21. Marques-Silva J, Sakallah K (1999) Grasp: A search algorithm for propositional satisfiability. IEEE Trans Comput 48(5):506–521

    Article  MathSciNet  Google Scholar 

  22. Marques-Silva JP, Sakallah KA (1999) The impact of branching heuristics in propositional satisfiability. Proc 9th Port Conf Artif Intell: 62–74

  23. Mathaikutty DA, Shukla SK, Kodakara SV, Lilja D, Dingankar A (2007) Design fault directed test generation for microprocessor validation. Proc Des, Autom Test Europe (DATE): 761–766

  24. Meyer R, Faber J, Hoenicke J, Rybalchenko A (2008) Model checking duration calculus: a practical approach. Form Asp Comput 20: 481–505

    Article  MATH  Google Scholar 

  25. MiniSAT. http://minisat.se/.

  26. Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: Engineering an efficient SAT solver. Proc Des Autom Conf (DAC): 530–535

  27. NuSMV. http://nusmv.irst.itc.it/.

  28. Shtrichman O (2000) Tuning SAT checkers for bounded model checking. Proc Comput Aided Verification (CAV): 480–494

  29. Strichman O (2001) Pruning techniques for the sat-based bounded model checking problem. Proc Correct Hardw Des Verification Methods (CHARME): 58–70

  30. Tille D, Eggersglüß S, Drechsler R (2010) Incremental solving techniques for SAT-based ATPG. IEEE Trans CAD Integr Circ Syst (TCAD) 29(7):1125–1130

    Article  Google Scholar 

  31. Wang C, Jin H, Hachtel GD, Somenzi F (2004) Refining the SAT decision ordering for bounded model checking. Proc Des Autom Conf (DAC): 535–538

  32. zChaff. http://www.princeton.edu/~chaff/zchaff.html.

  33. Zhang L, Prasad MR, Hsiao MS (2004) Incremental deductive and inductive reasoning for SAT-based bounded model checking. Proc Int Conf Comput-Aided Des (ICCAD): 502–509

Download references

Acknowledgments

This work was partially supported by NSF of China 61202103 and 91118007, Innovation Program of Shanghai Municipal Education Commission 14ZZ047, Open Project of SW/HW Co-design Engineering Research Center of MoE 2013001, and Shanghai Knowledge Service Platform Project ZF1213. This work was also partially supported by NSF grants CNS-0746261 and CCF-1218629. A preliminary version [7] of this paper appeared in the proceedings of Design, Automation and Test in Europe (DATE) 2011.

Author information

Authors and Affiliations

  1. Shanghai Key Lab of Trustworthy Computing, East China Normal University, Shanghai, 200062, China

    Mingsong Chen

  2. Department of Computer and Information Science and Engineering, University of Florida, Gainesville, FL, 32611, USA

    Xiaoke Qin & Prabhat Mishra

Authors
  1. Mingsong Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Xiaoke Qin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Prabhat Mishra
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mingsong Chen.

Additional information

Responsible Editor: M. Goessel

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Chen, M., Qin, X. & Mishra, P. Learning-oriented Property Decomposition for Automated Generation of Directed Tests. J Electron Test 30, 287–306 (2014). https://doi.org/10.1007/s10836-014-5452-x

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10836-014-5452-x

Keywords

Search

Navigation