Publication Type: Journal Article
Source: ACM Transactions on Design Automation of Electronic Systems, ACM, Volume 15, Issue 3, p.1-31 (2010)
; partial-order reduction
; Model Checking
; formal analysis
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 very precise formal race analysis by
means of Model Checking. Our compiler produces a simulator that uses the outcome of the
analysis to perform partial order reduction. The key insight to make the Model Checking engine
scale is to apply it only to tiny fractions of the SystemC model. We show that the outcome of the
analysis is not only valuable to eliminate redundant context switches at runtime, but can also be
used to diagnose race conditions statically. In particular, our analysis is able to reveal races that
can remain undetected during simulation and is able to formally prove the absence of races.