Speeding Up Simulation of SystemC Using Model Checking

Nicolas BlancDaniel Kroening

SystemC is a system-level modeling language that offers a wide range of features to describe concurrent systems. The SystemC standard permits simulators to implement a deterministic thread scheduling policy, which often hides concurrency-related design flaws. We present a novel compiler for SystemC that integrates a formal race analysis based on Model Checking techniques. The key insight to make the formal analysis scalable is to apply the Model Checker only to small partitions of the model. 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.This paper is an extended version of a conference paper that appeared at ICCAD 2008 [1]. This research is supported by ETH research grant TH-21/05-1 and by the Semiconductor Research Corporation (SRC) under contract no. 2006-TJ-1539.

Caso o link acima esteja inválido, faça uma busca pelo texto completo na Web: Buscar na Web

Biblioteca Digital Brasileira de Computação - Contato:
     Mantida por: