SystemC to Timed Automata Transformation Engine (STATE)

STATE takes a SystemC design as input and transforms it into a corresponding UPPAAL timed automata model. The transformation is based on a formal semantics defined for SystemC in [Her08],[Her10],[Her11],[Pockr11],[Pockr13],[Her13]. The general idea is to map the informally defined semantics of SystemC to the formally well-defined semantics of UPPAAL timed automata. This mapping defines a formal semantics for SystemC, and, at the same time, it enables the automatic transformation from a given SystemC design into a semantically equivalent UPPAAL timed automata model. The transformation preserves the informally defined semantics of SystemC completely. To ease debugging, it also keeps the structure of the original SystemC design transparent to the designer in the UPPAAL model (through prefixing). The current version of STATE supports structs, pointers, and arrays as well as the TLM 2.0 standard.

STATE is licenced under GPL and freely available. The examples described below are included in the zip file provided in the download section.

• Contents

  • Verification Flow
  • Assumptions
  • Implementation
  • Download STATE 2.1
  • Previous Releases
  • FIFO Example
  • Primitive Channel Example (sc_fifo)
  • ASR/ABS Example
  • Blocking Transport
  • Non-blocking Transport
  • AMBA Advanced High-performance Bus (AHB)

Verification Flow

Our tranformation from SystemC to UPPAAL enables the application of the UPPAAL model checker to SystemC designs. With that, it is possible to verify safety, liveness, and timing properties of a given SystemC design. The properties must be specified in a subset of CTL supported by UPPAAL. The model checker tries to verify the given property and yields satisfied or not satisfied. If the property turns out not to be satisfied, the model checker additionally generates a counter example, which can be visualized and animated in UPPAAL for debugging puroposes.
 

Assumptions

SystemC is a language that enables modeling and simulation of digital hardware and software components on different levels of abstraction. To this end, SystemC supports a very diverse set of models of computation. At the same time, as an extension of C++ , it inherits the full semantic scale of the C++ language. As the UPPAAL modeling language is less expressive than SystemC, we impose some restrictions on SystemC designs that can be transformed into a semantically equivalent UPPAAL model:

• The SystemC design can be constructed statically, i. e. it does not use process creation. Dynamic memory allocation is supported but currently disabled.
• All statements that are used for instantiation and binding must be evaluable at transformation time.
• We assume that no variables are shadowed (i. e. each variable has a unique identifier in its scope), and that no overloading of methods is used.
• The SystemC design may only use int, bool, data types that can be mapped to int and bool (e.g., bit vectors), structs and pointers without pointer arithmetics.
• No typecasts are used.
• No direct hardware access of memory addresses (e. g., int *p; p = 0xFFFFFF;).
• Structs are only referenced by pointers of the same type as the struct. This
• also means that there are no direct references to struct members.
• No recursion is used.
• No function pointers are used.
• We require that sockets are created statically, and that socket binding only takes place before elaboration time.
• The number of concurrent non-blocking transport requests must be bound by a statically determinable maximum (-maxpeq).

Implementation

STATE takes a SystemC design as input and yields a corresponding Uppaal model as output. As a front-end for SystemC, we used the Karlsruhe SystemC Parser (KaSCPar) [FZI]. KaSCPar parses a given SystemC design and generates an Abstract Syntax Tree (AST) in XML. The AST in XML serves as input for STATE, which generates a Uppaal model that is also in XML format and that can be used as input for the Uppaal tool suite. Figure 1 shows the tool chain from SystemC to Uppaal. Within STATE, the transformation of a given SystemC design is performed in two phases: first, the transformation engine constructs a Uppaal model from the given AST of the SystemC design. The model is incrementally build and stored in an internal representation. Second, the optimization engine performs several optimizations on that. Then, a UPPAAL model is written and can be used as input for the UPPAAL tool suite.

Download STATE 2.1

STATE 2.1 is released under GNU General Public License in Version 3. We provide the binaries as a jar file via direct download below. For the complete source code, please contact paula.herber [at] uni-muenster.de.

The input of STATE is the Abstract Syntax Tree (AST) of a SystemC design as generated by a silghtly modified version of the Karlsruhe SystemC Parser (KaSCPar), provided by the Karlsruhe Forschungszentrum Informatik (FZI). KaSCPar is licensed under GPL. Note that STATE only works with a slightly adapted version of the KaSCPar tool SC2AST, which also accepts and processes TLM keywords. As with STATE, we provide the binaries of our modified SC2AST tool as a jar file via direct download below. For the complete source code, please contact paula.herber [at] uni-muenster.de.

STATE 2.1 (zip file)

Previous Releases

STATE 1.0 and STATE 2.0 are released under GNU General Public License in Version 3. We provide the binaries as a jar file via direct download below. For the complete source code, please contact paula.herber [at]uni-muenster.de.

The input of STATE is the Abstract Syntax Tree (AST) of a SystemC design as generated by a silghtly modified version of the Karlsruhe SystemC Parser (KaSCPar), provided by the Karlsruhe Forschungszentrum Informatik (FZI). KaSCPar is licensed under GPL. Note that STATE only works with a slightly adapted version of the KaSCPar tool SC2AST, which also accepts and processes TLM keywords. As with STATE, we provide the binaries of our modified SC2AST tool as a jar file via direct download below. For the complete source code, please contact paula.herber [at]uni-muenster.de.

STATE is completely implemented in Java and should run on various operating systems. However, we only tested STATE 2.0 under Ubuntu 12.04 (Precise Pangolin) and Windows 8, and STATE 1.0 under Ubuntu 10.04 (Lucid Lynx) and Windows 7.
SC2AST requires gcc, sh, and the Xerces DOM Parser, available at http://xerces.apache.org/xerces2-j/. The jar file sc2ast.jar already contains a copy of the Xerces DOM Parser, which is licensed under the Apache Software License.

STATE 2.0 (zip file)

STATE 1.0 (zip file)

FIFO Example

In the FIFO example, a producer and a consumer communicate through a FIFO channel. It uses dynamic sensitivity and time, and also a synchronous clock. It is the best starting point to have a look at an automatically generated UPPAAL model, and also the first thing you should try when you installed our STATE binary.

Primitive Channel Example (sc_fifo)

The primitive channel example is very similar to the simple FIFO example. It only differs in that it uses the predefined primitive SystemC channel sc_fifo, which supports the request-update scheme. Thus, it is well-suited to see how primitive channels and update requests are handled in the resulting UPPAAL model.

ASR/ABS Example

The anti-slip regulation and anti-lock braking system (ASR/ABS) monitors the speed of each wheel and regulates the brake pressure in order to prevent wheel lockup or loss of traction and to improve the driver’s control over the car. It consists of dedicated wheel speed sensors, a hydraulic modulator to control the brake pressure, an electronic control unit that runs the control algorithms, and a control area network (CAN) bus. To measure the wheel speed, the number of incoming wheel signals (ticks) are used to compute the speed of each wheel. To this end, a tick counter is placed of each wheel. The measurement results are sent to an electronic control unit. On the ECU, the control algorithms for brake pressure control and Anti-Slip-Regulation (ASR) are executed. The resulting control signals are sent to the brake hydraulics. This is an abstract version, used for verification purposes. Note that this example must be transformed into a UPPAAL model with time resolution set to 100,000 to avoid an out-of-range error (option -tr 100000 for sc2uppaal).

Blocking Transport

The blocking transport example is a simple loosely-timed model in TLM 2.0 style, where a producer and a consumer communicate through a blocking transport with a delay of 10 ns. The blocking transport example uses sockets and temporal decoupling.

Non-blocking Transport

The non-blocking transport is an approximately-timed model in TLM 2.0 style, where a producer and a consumer communicate through a non-blocking transport. The non-blocking transport is implemented according to the TLM base protocol, i. e., it comprises four communication phases (init request, end request, init response and end response). The non-blocking transport requires sockets, temporal decoupling, and the full PEQ formalization.

AMBA Advanced High-performance Bus (AHB)

This TLM 2.0 implementation of the AMBA AHB was originally provided by Carbon Design Systems and only slightly modified. The Advanced Microcontroller Bus Architecture (AMBA) Bus is an on-a-chip bus introduced by ARM Ltd2 in 1996. The AMBA advanced high performance bus (AHB) protocol was introduced in 1999 and features burst transfers, split transactions and a bus width of up to 128 bits. Many high performance SoCs in a wide area of applications are currently using the AMBA AHB.

The architecture of the design is shown below. The tlm2 master initiates communications by sending read or write transactions via a blocking transport to the master to ahb module. The master to ahb module splits the given transaction into AMBA conform transfers and sends those over the bus according to the AMBA AHB protocol specification, i. e., with the correct timing, protocol phases, and transfer types. The AMBA AHB is a synchronous clocked bus.

The timing and arbitration of the AMBA AHB are described in the AMBA3 AHB-Lite Protocol Specification. An AMBA AHB transfer starts with a bus request asserted by a bus master. The arbiter collects all bus requests and sends a grant signal to one master. The granted bus master then drives the address and control signals. These signals provide information on the address, direction and width of the transfer, as well as an indication if the transfer forms part of a burst. AMBA AHB uses separate read and write buses to move data from slave to the master and the other way around. Every transfer consists of an address and control cycle and one or more cycles for the data. The TLM 2.0 implementation of the AMBA AHB provided by Carbon Design Systems implements this by multiple clocked non-blocking transports for each transfer. The design implements an arbiter and a decoder as specified in the Protocol Specification. The slave components receive transactions and read or write from/to memory, respectively.