Race Analysis for SystemC using Model Checking

Publication Type:

Conference Paper

Source:

ICCAD, IEEE, San Jose (2008)

URL:

http://www.kroening.com/publications/view-publications-bk2008-iccad.html

Abstract:

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.