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 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 dynam...

Full description

Saved in:
Bibliographic Details
Main Authors: Kundu, Sudipta, Ganai, Malay, Gupta, Rajesh
Format: Conference Proceeding
Language:English
Subjects:
Algorithm design and analysis
Analytical models
Computational modeling
Computing methodologies > Modeling and simulation > Model development and analysis
Computing methodologies > Modeling and simulation > Model development and analysis > Model verification and validation
Formal verification
Kernel
Object oriented modeling
Partial-Order Reduction
Safety
Simulation
State-space methods
System recovery
System testing
Testing
Verification
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0738-100X
DOI:10.1145/1391469.1391706