Race analysis for SystemC using model checking

SystemC is a system-level modeling language that offers a wide range of features to describe concurrent systems at different levels of abstraction. The SystemC standard permits simulators to implement a deterministic scheduling policy, which often hides concurrency-related design flaws. We present a novel compiler for SystemC that integrates a formal and scalable race analysis. This analysis combines both classic static analysis and model checking techniques. The outcome of the analysis is not only valuable to diagnose the effect of race conditions, but can also be used to improve simulation performance dramatically. Our compiler produces a simulator that uses the race analysis information at runtime to perform partial-order reduction, thereby eliminating context switches that do not affect the result of the simulation. Experimental results show simulation speedups of one order of magnitude and better.