Title: Compositional reactive semantics of system-level designs written in SystemC and formal verification with predicate abstraction
Authors: Nesrine Harrath; Bruno Monsuez
Department of Electronics and Computer Engineering, ENSTA ParisTech, 828 Boulevard des Marchaux, 91762 Palaiseau, France; CNAM-CEDRIC, 292 Rue St Martin, FR-75141 Paris Cedex 03, France
Department of Electronics and Computer Engineering, ENSTA ParisTech, 828 Boulevard des Marchaux, 91762 Palaiseau, France
Abstract: In this paper, we propose a method to automatically extract an abstract representation of SystemC components into the SystemC-waiting state automata: a compositional formal model for verifying properties of SystemC at the transaction level within a delta-cycle. The main drawback of this model as mentioned in previous works was that it should be provided manually. In this paper, we propose a method to automatically build the SystemC waiting-state automata from the SystemC code. First, we select a subset of SystemC language and define its operational semantics that succinctly captures its reactive features and allows the specification of synchronous and asynchronous communications between the communicating components. Next, we symbolically execute the SystemC code using these semantics to generate the set of all possible traces and finally we use predicate abstraction to reduce the complexity of the generated graph during symbolic execution. We illustrate the use of symbolic execution and then predicate abstraction for two examples of SystemC programs: one that handles execution traces without loops and another one that handles loops.
Keywords: SystemC; operational semantics; symbolic execution; predicate abstraction; compositional verification.
Int. J. of Critical Computer-Based Systems, 2014 Vol.5, No.3/4, pp.268 - 299
Available online: 03 Sep 2014