Nothing Special   »   [go: up one dir, main page]
Skip to main content

Advertisement

Springer Nature Link
Log in

Verification of SpecC using predicate abstraction

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

Languages such as SystemC or SpecC offer modeling of hardware and whole system designs at a high level of abstraction. However, formal verification techniques are widely applied in the hardware design industry only for low level designs, such as a netlist or RTL. The higher abstraction levels offered by these new languages are not yet amenable to rigorous, formal verification. This paper describes how to apply predicate abstraction to SpecC system descriptions. The technique supports the concurrency constructs offered by SpecC. It models the bit-vector semantics of the language accurately, and can be used both for property checking and for checking refinement together with a traditional low-level design given in Verilog.

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

Similar content being viewed by others

Notes

  1. We are grateful to Masahiro Fujita for clarifying this issue.

  2. Thus, we implement a form of busy-waiting—this is wasteful if execution is the goal, but simplifies the model if the goal is model checking.

  3. http://www.inf.ethz.ch/personal/daniekro/satabs/

References

  1. SystemC, http://www.systemc.org

  2. Alur R, Henzinger TA, Mang F, Qadeer S, Rajamani SK, Tasiran S (1998) Mocha: Modularity in model checking. In: Proceedings of the 10th international conference on computer-Aided verification (CAV), vol 1427 of Lecture notes in computer science, pp 521–525

  3. Ball T, Chaki S, Rajamani SK (2001) Parameterized verification of multithreaded software libraries. In: Proceedings of the 7th international conference on tools and algorithms for the construction and analysis of systems (TACAS), vol 2031 of lecture notes in computer science, pp 158–173

  4. Ball T, Rajamani SK (2000) Boolean programs: A model and process for software analysis. Technical Report 2000-14, Microsoft Research

  5. Ball, T, Rajamani SK (2001) Automatically validating temporal safety properties of interfaces. In: The 8th International SPIN workshop on model checking of software, vol 2057 of lecture notes in computer science, pp 103–122

  6. Biere A, Cimatti A, Clarke EM, Fujita M, Yhu Y (1999a) Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of the 36th conference on design automation conference (DAC), pp 317–320

  7. Biere A, Cimatti A, Clarke EM, Yhu Y (1999b) Symbolic model checking without BDDs. In: Proceedings of the 5th international conference on tools and algorithms for construction and analysis of systems (TACAS), vol 1579 of lecture notes in computer science, pp 193–207

  8. Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142–170

    Google Scholar 

  9. Chaki S, Clarke E, Groce A, Ouaknine J, Strichman O, Yorav K (2004) Efficient verification of sequential and concurrent C programs. Form Meth Syst Des (FMSD) 25(2–3):129–166

    Google Scholar 

  10. Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV Version 2: An opensource tool for symbolic model checking. In: Proceedings of the 14th international conference on computer aided verification (CAV), vol 2404 of lecture notes in computer science, pp 359–364

  11. Clarke E, Grumberg O, Peled D (1999) Model checking. MIT Press

  12. Clarke E, Grumberg O, Talupur M, Wang D (2003) High level verification of control intensive systems using predicate abstraction. In: Proceedings of the 1st ACM and IEEE international conference on formal methods and models for co-design (MEMOCODE), pp 55–64

  13. Clarke E, Kroening D, Sharygina N, Yorav K (2004) Predicate abstraction of ANSI-C programs using SAT. Formal Methods Syst Des (FMSD) 25:105–127

    Google Scholar 

  14. Clarke E, Kroening D, Sharygina N, Yorav K (2005) SATABS: SAT-based predicate abstraction for ANSI-C. In: Proceedings of the 11th international conference on tools and algorithms for the construction and analysis of systems (TACAS), vol 3440 of lecture notes in computer science, pp 570–574

  15. Clarke EM, Emerson EA (1981) Synthesis of synchronization skeletons for branching time temporal logic. In: Logic of programs: Workshop, vol 131 of Lecture notes in computer science, pp 52–71

  16. Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Proceedings of the 12th international conference on computer aided verification (CAV), vol 1855 of lecture notes in computer science, pp 154–169

  17. Clarke EM, Grumberg O, Long DE (1992) Model checking and abstraction. In: Proceedings of the 19th symposium on principles of programming languages (POPL), pp 342–354

  18. Cook B, Kroening D, Sharygina N (2005a) Cogent: Accurate theorem proving for program verification. In: Etessami K, Rajamani SK (eds) Proceedings of the 19th international conference on computer aided verification (CAV), vol. 3576 of lecture notes in computer science, pp 296–300

  19. Cook B, Kroening D, Sharygina N (2005b) Symbolic model checking for asynchronous boolean programs. In: Godefroid P (ed) Proceedings of the 12th international SPIN workshop, vol 3639 of lecture notes in computer science, pp 75–90

  20. Copty F, Fix L, Fraer R, Giunchiglia E, Kamhi G, Tacchella A, Vardi MY (2001) Benefits of bounded model checking at an industrial setting. In: Berry G, Comon H, Finkel A (eds) Proceedings of the 13th international conference on computer aided verification (CAV), pp 436–453

  21. Detlefs D, Nelson G, Saxe JB (2003) Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs

  22. Dijkstra E (1976) A discipline of programming. Prentice Hall

  23. Dömer R, Gerstlauer A, Gajski D (2002) SpecC language reference manual, Version 2.0. http://www.specc.org/

  24. Flanagan C, Godefroid P (2005) Dynamic partial-order reduction for model checking software. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL), pp 110–121

  25. Graf S, Saïdi H (1997) Construction of abstract state graphs with PVS. In: Grumberg O (ed) Proceedings of the 9th international conference on computer aided verification (CAV), vol 1254 of lecture notes in computer science, pp 72–83

  26. Henzinger TA, Jhala R, Majumdar R, Qadeer S (2003) Thread modular abstraction refinement. In: Proceedings of the 15th international conference on computer-aided verification (CAV), vol 2725 of lecture notes in computer science, pp 262–274

  27. Holzmann GJ (1997) The model checker SPIN. IEEE Trans Softw Eng 23(5):279–295

    Google Scholar 

  28. Holzmann GJ, Peled D (1994) An improvement in formal verification. In: Proceedings of the 7th IFIP WG6.1 international conference on formal description techniques, pp 197–211

  29. Jain H, Clarke E, Kroening D (2004) Verification of SpecC and verilog using predicate abstraction. In: Proceedings of the 2nd ACM and IEEE international conference on formal methods and models for co-design (MEMOCODE), pp 7–16

  30. Jain H, Kroening D, Sharygina N, Clarke E (2005) Word level predicate abstraction and refinement for verifying RTL Verilog. In: Proceedings of the 42nd design automation conference (DAC), pp 445–450

  31. Jhala R, McMillan KL (2006) A practical and complete approach to predicate refinement. In: TACAS, vol. 3920 of lecture notes in computer science, pp 459–473

  32. Kroening, D, Clarke E (2004) Checking consistency of C and Verilog using predicate abstraction and induction. In: Proceedings of the 2004 IEEE/ACM international conference on computer-aided design (ICCAD), pp 66–72

  33. Kroening D, Clarke E, Yorav K (2003) Behavioral consistency of C and Verilog programs using bounded model checking. In: Proceedings of the 40th design automation conference (DAC), pp 368–371

  34. Kroening D, Sharygina N (2005) Formal verification of system C by automatic hardware/software partitioning. In: Proceedings of the 3rd ACM and IEEE international conference on formal methods and models for co-design (MEMOCODE), pp 101–110

  35. Kroening D, Strichman O (2003) Efficient computation of recurrence diameters. In: Zuck L, Attie P, Cortesi A, Mukhopadhyay S (eds) Proceedings of the 4th international conference on verification, model checking, and abstract interpretation (VMCAI), vol 2575 of lecture notes in computer science, pp 298–309

  36. Ku, D, DeMicheli G (1990) HardwareC—A language for hardware design (Version 2.0). Technical Report CSL-TR-90-419, Stanford University

  37. Kurshan RP (1994) Computer-aided verification of coordinating processes: The automata-theoretic approach. Princeton University Press

  38. Matsumoto T, Saito H, Fujita M (2003) Equivalence checking of C based hardware descriptions by using symbolic simulation and program slicer. In: International workshop on logic and synthesis (IWLS'03)

  39. McMillan K: CMU Symbolic Model Verifier, http://www.cs.cmu.edu/~modelcheck/smv.html

  40. Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th design automation conference (DAC), pp 530–535

  41. Mueller W, Dömer R, Gerstlauer A (2002) The formal execution semantics of specC. In: Proceedings of the 15th international symposium on system synthesis, pp 150–155

  42. Page I (1996) Constructing hardware-software systems from a single description. J VLSI Signal Process 12(1):87–107

    Google Scholar 

  43. Pnueli A, Shtrichman O, Siegel M (1998) The code validation tool CVT: Automatic verification of a compilation process. Int J Softw Tools Technol Transf (STTT) 2(2):192–201

    Google Scholar 

  44. Qadeer S, Rajamani SK, Rehof J (2004) Summarizing procedures in concurrent programs. In: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL), pp 245–255

  45. Qadeer, S, Rehof J (2005) Context-bounded model checking of concurrent software. In: Proceedings of the 11th international conference on tools and algorithms for the construction and analysis of systems (TACAS), vol 3440 of lecture notes in computer science, pp 3–107

  46. Rabinovitz I, Grumberg O (2005) Bounded model checking of concurrent programs. In: Proceedings of the 17th international conference on computer aided verification (CAV), vol 3576 of lecture notes in computer science, pp 82–97

  47. Séméria L, Seawright A, Mehra R, Ng D, Ekanayake A, Pangrle B (2002) RTL C-based methodology for designing and verifying a multi-threaded processor. In: Proceedings of the 39th design automation conference (DAC), pp 123–128

  48. Shtrichman O (2000) Tuning SAT checkers for bounded model checking. In: Emerson E, Sistla A (eds) Proceedings of the 12th international conference on computer aided verification (CAV), pp 480–494

Download references

Acknowledgments

We thank Masahiro Fujita for numerous clarifications of the semantics of SpecC, and the anonymous referees for helpful suggestions.

Author information

Authors and Affiliations

  1. Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA

    Edmund Clarke & Himanshu Jain

  2. Computer Systems Institute, ETH Zurich, Switzerland

    Daniel Kroening

Authors
  1. Edmund Clarke
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Himanshu Jain
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Daniel Kroening
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Edmund Clarke.

Additional information

This paper is an extended version of [29].

This research was sponsored by the Gigascale Systems Research Center (GSRC) under contract no. 9278-1-1010315, the National Science Foundation (NSF) under grant no. CCR-9803774, the Office of Naval Research (ONR), the Naval Research Laboratory (NRL) under contract no. N00014-01-1-0796, the Army Research Office (ARO) under contract no. DAAD19-01-1-0485, and the General Motors Collaborative Research Lab at CMU. The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of GSRC, NSF, ONR, NRL, ARO, GM, or the U.S. government.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Clarke, E., Jain, H. & Kroening, D. Verification of SpecC using predicate abstraction. Form Method Syst Des 30, 5–28 (2007). https://doi.org/10.1007/s10703-006-0020-3

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-006-0020-3

Keywords

Search

Navigation