Software Model Checking SystemC

SystemC is an increasingly used language for writing executable specifications of systems-on-chip. The verification of SystemC, however, is a very difficult challenge. Simulation features great scalability, but can miss important defects. On the other hand, formal verification of SystemC is extremely hard because of the presence of threads, and the intricacies of the communication and scheduling mechanisms. In this paper, we explore formal verification for SystemC by means of software model checking techniques, which have demonstrated substantial progress in recent years. We propose an accurate model of SystemC and three complementary encodings of SystemC to finite-state processes, sequential and threaded programming models. We implement the proposed approaches in a tool chain and carry out a thorough experimental evaluation using several benchmarks taken from the literature on SystemC verification, and experimenting with different state-of-the-art software model checkers. The results clearly show the applicability and efficiency of the proposed approaches. In particular, the results show the effectiveness of the threaded and of the finite-model encodings to prove and disprove properties, respectively.