Partial order reduction for scalable testing of systemC TLM designs

ABSTRACT

A SystemC simulation kernel consists of a deterministic implementation of the scheduler, whose specification is non-deterministic. To leverage testing of a SystemC TLM design, we focus on automatically exploring all possible behaviors of the design for a given data input. We combine static and dynamic partial order reduction techniques with SystemC semantics to intelligently explore a subset of the possible traces, while still being provably sufficient for detecting deadlocks and safety property violations. We have implemented our exploration algorithm in a framework called Satya and have applied it to a variety of examples including the TAC benchmark. Using Satya, we automatically found an assertion violation in a benchmark distributed as a part of the OSCI repository.

REFERENCES

• 1: Edison Design Group (EDG) C/C++ Front End, 1992. www.edg.com.
• 2: IEEE Standard 1666 SystemC Language Reference Manual, 2005. www.systemc.org.
• 3: ST Microelectronics Transaction Accurate Communication (TAC) platform, 2005. www.greensocs.com/TACPackage.
• 4: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 5: Lukai Cai , Daniel Gajski, Transaction level modeling: an overview, Proceedings of the 1st IEEE/ACM/IFIP international conference on Hardware/software codesign and system synthesis, October 01-03, 2003, Newport Beach, CA, USA [doi>10.1145/944645.944651]
• 6: M. Dwyer and J. Hatcliff. Slicing software for model construction. In ACM Workshop on PEPM, 1999.
• 7: Cormac Flanagan , Patrice Godefroid, Dynamic partial-order reduction for model checking software, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.110-121, January 12-14, 2005, Long Beach, California, USA
• 8: M. Girkar , C. D. Polychronopoulos, Automatic Extraction of Functional Parallelism from Ordinary Programs, IEEE Transactions on Parallel and Distributed Systems, v.3 n.2, p.166-178, March 1992 [doi>10.1109/71.127258]
• 9: P. Godefroid. Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. PhD thesis, Univerite De Liege, 1995.
• 10: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
• 11: Daniel Große , Rüdiger Ebendt , Rolf Drechsler, Improvements for constraint solving in the systemc verification library, Proceedings of the 17th ACM Great Lakes symposium on VLSI, March 11-13, 2007, Stresa-Lago Maggiore, Italy [doi>10.1145/1228784.1228901]
• 12: Thorsten Grotker, System Design with SystemC, Kluwer Academic Publishers, Norwell, MA, 2002
• 13: Ali Habibi , Sofiene Tahar, Design for Verification of SystemC Transaction Level Models, Proceedings of the conference on Design, Automation and Test in Europe, p.560-565, March 07-11, 2005 [doi>10.1109/DATE.2005.112]
• 14: C. Helmstetter , F. Maraninchi , L. Maillet-Contoz , M. Moy, Automatic Generation of Schedulings for Improving the Test Coverage of Systems-on-a-Chip, Proceedings of the Formal Methods in Computer Aided Design, p.171-178, November 12-16, 2006 [doi>10.1109/FMCAD.2006.10]
• 15: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 16: D. Kroening , N. Sharygina, Formal verification of SystemC by automatic hardware/software partitioning, Proceedings of the 2nd ACM/IEEE International Conference on Formal Methods and Models for Co-Design, p.101-110, July 11-14, 2005 [doi>10.1109/MEMCOD.2005.1487900]
• 17: S. Meftali, J. Vennin, and J.-L. Dekeyser. A fast SystemC simulation methodology fo Multi-Level IP/SoC design. In IFIP Intl. Workshop on IP Based SoC Design, 2003.
• 18: Moy , Maraninchi , Maillet-Contoz, LusSy: A Toolbox for the Analysis of Systems-on-a-Chip at the Transactional Level, Proceedings of the Fifth International Conference on Application of Concurrency to System Design, p.26-35, June 07-09, 2005 [doi>10.1109/ACSD.2005.23]
• 19: Alper Sen , Vijay K. Garg, Formal Verification of Simulation Traces Using Computation Slicing, IEEE Transactions on Computers, v.56 n.4, p.511-527, April 2007 [doi>10.1109/TC.2007.1011]
• 20: R. Shyamasundar, F. Doucet, R. Gupta, and I. Kruger. Compositional reactive semantics of SystemC and verification with RuleBase. In Proceedings of the GM R&D Workshop, 2007.
• 21: Stuart Swan, SystemC transaction level models and RTL verification, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA [doi>10.1145/1146909.1146937]
• 22: Moshe Y. Vardi, Formal techniques for SystemC verification, Proceedings of the 44th annual conference on Design automation, June 04-08, 2007, San Diego, California [doi>10.1145/1278480.1278527]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.4 Model Validation and Analysis

General Terms:
Algorithms, Design, Verification

Keywords:
partial-order reduction, simulation, testing, verification