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