0 Blanc, N. Kroening, D 2010 Race Analysis for SystemC using Model Checking ACM Transactions on Design Automation of Electronic Systems ACM 15 3 1-31 05/2010 SystemC, simulation, partial-order reduction, Model Checking, formal analysis <div>&nbsp;SystemC is a system-level modeling language that offers a wide range of features to describe</div><div>concurrent systems at different levels of abstraction. The SystemC standard permits simulators</div><div>to implement a deterministic scheduling policy, which often hides concurrency-related design flaws.</div><div>We present a novel compiler for SystemC that integrates a very precise formal race analysis by</div><div>means of Model Checking. Our compiler produces a simulator that uses the outcome of the</div><div>analysis to perform partial order reduction. The key insight to make the Model Checking engine</div><div>scale is to apply it only to tiny fractions of the SystemC model. We show that the outcome of the</div><div>analysis is not only valuable to eliminate redundant context switches at runtime, but can also be</div><div>used to diagnose race conditions statically. In particular, our analysis is able to reveal races that</div><div>can remain undetected during simulation and is able to formally prove the absence of races.</div><p>&nbsp;</p> http://www.kroening.com/publications/view-publications-bk2010-todaes.html