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

• Type: Conference
• Year: 2008
• Where: ICCAD
• Authors: Nicolas Blanc, Daniel Kroening
• Keywords: Classic Static Analysis, Hardware, ICCAD 2008, Race Analysis Information, Scalable Race Analysis