Partial order reduction for scalable testing of systemC TLM designs

A SystemC simulation kernel consists of a deterministic implementation of the scheduler, whose specification is nondeterministic. 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. Categories and Subject Descriptors I.6.4 [Computing Methodologies]: Simulation and Modeling--Model Validation and Analysis General Terms Algorithms, Design and Verification Keywords Partial-Order Reduction, Verification...

• Type: Conference
• Year: 2008
• Where: DAC
• Authors: Sudipta Kundu, Malay K. Ganai, Rajesh Gupta
• Keywords: DAC 2008, Design Automation, SystemC Semantics, SystemC Simulation Kernel, SystemC TLM Design