Formal techniques for SystemC verification

ABSTRACT

SystemC has emerged lately as a de facto, open, industry standard modeling language, enabling a wide range of modeling levels, from RTL to system level. Its increasing acceptance is driven by the increasing complexity of designs, pushing designers to higher and higher levels of abstractions.

While a major goal of SystemC is to enable verification at higher level of abstraction, enabling early exploration of system-level designs, the focus so far has been on traditional dynamic validation techniques. It is fair to see that the development of formal-verification techniques for SystemC models is at its infancy. In spite of intensive recent activity in the development of formal-verification techniques for software, extending such techniques to SystemC is a formidable challenge. The difficulty stems from both the object-oriented nature of SystemC, which is fundamental to its modeling philosophy, and its sophisticated event-driven simulation semantics.

In this position paper we discuss what is needed to develop formal techniques for SystemC verification, augmenting dynamic validation techniques. By formal techniques we refer here to a range of techniques, including assertion-based dynamic validation, symbolic simulation, formal test generation, explicit-state model checking, and symbolic model checking.

REFERENCES

• 1: R. Armoni, D. Korchemny, A. Tiemeyer, and M. V. Y. Zbar. Deterministic dynamic monitors for linear-time assertions. In Proc. Workshop on Formal Approaches to Testing and Runtime Verification, volume 4262 of Lecture Notes in Computer Science. Springer, 2006.
• 2: T. Ball, B. Cook, V. Levin, and S. Rajamani. SLAM and static driver verifier: Technology transfer of formal methods inside microsoft. In Proc. 4th Int'l Conf. on Integrated Formal Methods, Lecture Notes in Computer Science 2999, pages 1--20, 2004.
• 3: M. Barnett, R. DeLine, M. Fähndrich, K. Leino, and W. Schulte. Verification of object-oriented programs with invariants. J. of Object Technology, 3(6), 2004.
• 4: B. Bentley, High level validation of next-generation microprocessors, Proceedings of the Seventh IEEE International High-Level Design Validation and Test Workshop, p.31, October 27-29, 2002
• 5: Gérard Berry , Georges Gonthier, The ESTEREL synchronous programming language: design, semantics, implementation, Science of Computer Programming, v.19 n.2, p.87-152, Nov. 1992 [doi>10.1016/0167-6423(92)90005-V]
• 6: Jerry R. Burch , David L. Dill, Automatic verification of Pipelined Microprocessor Control, Proceedings of the 6th International Conference on Computer Aided Verification, p.68-80, June 21-23, 1994
• 7: Lilian Burdy , Yoonsik Cheon , David R. Cok , Michael D. Ernst , Joseph R. Kiniry , Gary T. Leavens , K. Rustan M. Leino , Erik Poll, An overview of JML tools and applications, International Journal on Software Tools for Technology Transfer (STTT), v.7 n.3, p.212-232, June 2005 [doi>10.1007/s10009-004-0167-4]
• 8: William R. Bush , Jonathan D. Pincus , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H]
• 9: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 10: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 11: N. Dave. Designing a reorder buffer in Bluespec. In Proc. 2nd ACM/IEEE Int'l Conf. on Formal Methods and Models for Co-Design, pages 93--102, 2004.
• 12: Rolf Drechsler , Daniel Groβe, Reachability Analysis for Formal Verification of SystemC, Proceedings of the Euromicro Symposium on Digital Systems Design, p.337, September 04-06, 2002
• 13: Cindy Eisner , Dana Fisman, A Practical Introduction to PSL (Series on Integrated Circuits and Systems), Springer-Verlag New York, Inc., Secaucus, NJ, 2006
• 14: Harry Foster , David Lacey , Adam Krolnik, Assertion-Based Design, Kluwer Academic Publishers, Norwell, MA, 2003
• 15: A. Gawanmeh, A. Habibi, and S. Tahar. Enabling SystemC verification using abstract state machines. In Proc. Languages for Formal Specification and Verification, Forum on Specification and Design Languages, 2004.
• 16: Daniel D. Gajski , Rainer Domer , Junyu Peng , Andreas Gerstlauer, System Design: A Practical Guide with Specc, Kluwer Academic Publishers, Norwell, MA, 2001
• 17: R. Goering. A call to action for the EDA industry. EETimes, June 2005.
• 18: Thorsten Grotker, System Design with SystemC, Kluwer Academic Publishers, Norwell, MA, 2002
• 19: D. Große and R. Drechsler. Formal verification of LTL formulas for SystemC designs. In Proc. Int'l Symposium on Circuits and Systems, pages 245--248, 2003.
• 20: D. Große and R. Drechsler. Checkers for SystemC designs. In Proc. 2nd ACM/IEEE Int'l Conf. on Formal Methods and Models for Co-Design, pages 171--178, 2004.
• 21: K. Havelund and T. Pressburger. Model checking JAVA programs using JAVA pathfinder. Int'l J. on Software Tools for Technology Transfer, 2(4):366--381, 2000.
• 22: Warren A. Hunt, Jr. , Jun Sawada, Verifying the FM9801 Microarchitecture, IEEE Micro, v.19 n.3, p.47-55, May 1999 [doi>10.1109/40.768503]
• 23: C. Ip and S. Swan. A tutorial introduction on the new SystemC verification standard. Technical report, www.systemc.org, 2003. White Paper.
• 24: Z. Khasidashvili , M. Skaba , D. Kaiss , Z. Hanna, Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.58-65, November 07-11, 2004 [doi>10.1109/ICCAD.2004.1382543]
• 25: James C. King, Symbolic execution and program testing, Communications of the ACM, v.19 n.7, p.385-394, July 1976 [doi>10.1145/360248.360252]
• 26: Shuvendu K. Lahiri , Sanjit A. Seshia , Randal E. Bryant, Modeling and Verification of Out-of-Order Microprocessors in UCLID, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.142-159, November 06-08, 2002
• 27: Leslie Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2002
• 28: James Monaco , David Holloway , Rajesh Raina, Functional verification methodology for the PowerPC 604 microprocessor, Proceedings of the 33rd annual conference on Design automation, p.319-324, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240579]
• 29: J. Ruf , D. Hoffmann , J. Gerlach , T. Kropf , W. Rosenstiehl , W. Mueller, The simulation semantics of systemC, Proceedings of the conference on Design, automation and test in Europe, p.64-70, March 2001, Munich, Germany
• 30: Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748-752, June 15-18, 1992
• 31: C. Pasareanu and W. Visser. Verification of Java programs using symbolic execution and invariant generation. In Proc. 11th Int'l SPIN SWorkshop on Model Checking Software, volume 2989 of Lecture Notes in Computer Science, pages 164--181. Springer, 2004.
• 32: T. Ramanathan and V. Thomas. Platform 2015: Intel processor and platform evolution for the next decade. Technical report, Intel, 2005. White Paper, Platform 2015.
• 33: A. Raynaud. Code coverage techniques - a hands-on view. EETimes, February 2003.
• 34: L. Singh and L. Drucker. Advanced Verification Techniques: A SystemC Based Approach for Successful Tapeout. Springer, 2004.
• 35: Stuart Sutherland , Simon Davidmann , Peter Flake , P. Moorby, SystemVerilog for Design: A Guide to Using SystemVerilog for Hardware Design and Modeling, Springer-Verlag New York, Inc., Secaucus, NJ, 2006
• 36: S. Vijayaraghavan and M. Ramanathan. A Practical Guide for SystemVerilog Assertions. Springer, 2005.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.2 Design Aids

Additional Classification:
  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING

General Terms:
Verification

Keywords:
formal verification, high-level model