A framework for verification of SystemC designs using SystemC waiting state automata

Abstract

The SystemC waiting-state automaton is a compositional abstract formal model for verifying properties of SystemC at the transaction level within a delta-cycle: the smallest simulation unit time in SystemC. In this chapter, how to extract automata for SystemC components where we distinguish between threads and methods in SystemC. Then, we propose an approach based on a combination of symbolic execution and computing fixed points via predicate abstraction to infer relations between predicates generated during symbolic execution. Finally, we define how to apply model checking to prove the correctness of the abstract analysis.