State - A Systemc To Timed Automata Transformation Engine

SystemC is a system level design language that is widely used in hardware/software codesign. As the semantics of SystemC is only informally defined, verification of SystemC designs is mainly done using simulation and testing. With that, faults can be detected but it is impossible to verify the correctness of a given system for all possible executions. In this paper, we present our SystemC to Timed Automata Transformation Engine. STATE takes a SystemC design as input and transforms it into a UPPAAL timed automata model. This enables automated formal verification of SystemC designs using the UPPAAL model checker. To ease debugging, the transformation keeps the structure of the original SystemC design transparent to the designer in the resulting UPPAAL model. The current version of STATE supports many relevant SystemC language elements, including complex interactions between processes, dynamic sensitivity and timing behavior, structs, arrays, pointers, as well as the TLM 2.0 standard. We demonstrate the practical applicability of STATE with three case studies, including an industrial design of an AMBA bus.