SystemC is widely used in hardware/software codesign. Although it is also used for the design of safety-critical applications, existing formal veri cation techniques for SystemC are still hardly used in industrial practice. The main reasons for this are scalability issues, the lacking support for many practically relevant SystemC language constructs, and that counter-examples are not always easy to use for debugging. In this paper, we present an approach for the formal veri cation of SystemC designs using the BLAST model checker. The main advantages of our approach are: First, we enable a fully automatic veri cation of SystemC designs that makes use of counter-example guided abstraction re nement. Second, we support a large subset of SystemC, including pointers, arrays, and structs. Third, we ease debugging by keeping the structure of the design transparent to the designer. We demonstrate the applicability of our approach with experimental results from an Anti-Slip Regulation and Anti-Lock Braking system.
Embedded systems are often used in domains where a failure results in high
nancial losses or even in serious injury or death, e. g., in cars, airplanes and
transportation systems. This makes it indispensable to ensure their correctness
with systematic and comprehensive veri cation techniques. At the same time,
embedded systems typically consist of deeply integrated hardware and software
components, which makes comprehensive veri cation a di cult challenge. A
language that is widely used for modeling such systems is the system level design
language SystemC [
In this paper, we present an approach for the formal veri cation of SystemC
designs using the software model checker BLAST [
The rest of this paper is structured as follows: In the next section, we brie y introduce the preliminaries that are necessary for understanding the remainder of the paper. In Section 3, we summarize related work. In Section 4, we present the main contribution of this paper, namely our approach for the formal veri cation of SystemC designs using the BLAST model checker. We present experimental results in Section 5 and conclude in Section 6. 2
In this section, we brie y introduce the preliminaries that are necessary to understand the remainder of the paper. 2.1
SystemC is a system-level design language and a framework for HW/SW
cosimulation. The semantics of SystemC is informally de ned in an IEEE
standard [
Like typical hardware description languages, SystemC supports the notion of
delta-cycles, which impose a partial order on parallel processes. This means that
the execution is split into an evaluate and an update phase. In the rst phase,
concurrent processes are evaluated. This may include read and write accesses to
so-called primitive channels, which store changes in temporary variables and do
not update their channel state until the update phase. This ensures that although
the processes are serialized, they all work on the same channel states (i. e., input
data). A delta-cycle lasts an in nitesimal amount of time, and an arbitrary,
nite number of delta-cycles may be executed at one point in simulation time.
Note that the order in which processes are executed within a delta-cycle is not
speci ed in [
There exist several approaches to provide a formal semantics for SystemC. Many
of them rely on the transformation of SystemC designs into some sort of state
machine, e.g. [
Besides Kroening et al. [
In our own previous work, we have presented an approach for the
transformation of SystemC designs into UPPAAL timed automata and their veri cation
using the UPPAAL model checker [
The main contribution of this paper is a transformation from SystemC into nondeterministic sequential C that keeps the structure of the design transparent to the designer. The resulting C program can be veri ed using the BLAST model checker. The main idea of the transformation is that we interpret the SystemC semantics in sequential C code, using the non-deterministic choice of the BLAST model checker to model the SystemC scheduler. To this end, we transform each SystemC process of a given design into a set of C methods, whose execution is controlled by C implementations of the (non-deterministic) scheduler, events, and sensitivity. Our transformation supports a large subset of SystemC programs, including static and dynamic sensitivity, time, pointers, arrays, and structs. In the following subsections, we rst de ne this subset by a set of assumptions we have to impose on a given input design. Then, we explain how a SystemC design is represented as a C program using our interpretation of its semantics. Finally, we describe our implementations of methods, events, processes, the scheduler and the request-update mechanism of primitive channels. 4.1
We impose the following assumptions on a given input design: 1. No recursion is used. 2. No function pointers are used. 3. We assume that pointer arithmetic is used safely and that type safety of memory accesses is given. 4. We assume that no integer over ows are present in the system. 5. So far, we do not support any hardware data types. 6. So far, we do not support class inheritance.
The rst four assumptions are directly derived from the subset of C programs that is supported by the BLAST model checker. Assumptions 5 and 6 could potentially be lifted in future work. 4.2
The main challenge for the transformation from SystemC into non-deterministic sequential C programs is to interpret the SystemC execution semantics and nd an adequate representation of each SystemC language construct in the resulting C program. The SystemC execution semantics is de ned by the interplay between the scheduler, processes, events, and primitive channels. In particular, the execution of processes is controlled by events and the scheduler. A process may be interrupted by a wait call, which results in the suspension of the process until it is triggered by an event or the expiration of a given timeout. To model this behavior in a C program, it is necessary to implement interrupt routines, which are able to save the current state of a process, suspend its execution and resume it at a later point of execution.
call
Methods from all modules and channels
interrupt handling suspend Processes process state sensitivity type activate update
notify
Events event state notification delay notify update Scheduler notify
Support variables Member variables Primitive Channels request_update() request−update−flag activate update g // s e t dynamic s e n s i t i v i t y d y n s e n s i t i v i t y [ p id ] = ev ; . . . 4.3
Listing 1.1. Transformation of Event Noti cation The structure of a SystemC design is de ned by modules that are connected via ports and channels. Each of the modules and channels contains local variables, events, methods and processes, and possibly other modules or channels. In contrast to SystemC, C does not support object-orientation. To cope with this, we atten the hierarchy of a given SystemC design and translate all methods and variables into global methods and variables. We keep the structure of the original design transparent to the designer using pre xing. Port connections are implicitly modeled by replacing the call of a method through a port with a call to the channel method that is bound to this port.
As stated above, the SystemC execution semantics is de ned by the interplay
of the scheduler, events, and processes. The main challenge when modeling the
SystemC scheduler in a sequential C program is to resolve concurrent processes
into a sequential execution order. Following the approach of [
For illustration, we use a simple producer-consumer example, where a producer and a consumer communicate through a rst-in- rst-out (FIFO) bu er. Both the producer and the consumer have a main method, which is bound to a process. Additionally, the producer has a method produce, which is called from the main method and produces an item.
Event Transformation As in [
An example of a timed noti cation of an event ev is shown in Lines 5 to 8 in Listing 1.2. The semantics of SystemC event noti cations dictates that a timed noti cation overwrites pending timed noti cations if the given timing delay expires earlier than the pending noti cation. A timed noti cation is discarded if a delta-delay noti cation is pending. We check these two conditions in Lines 5-6. The event sensitivity is set to dynamic in Line 11.
Process Suspension and Resumption To model event-triggered execution, we
have to cope with suspension and resumption of processes. For example, in the
producer-consumer design, the method produce is suspended after timed
notication. In order to enable the suspension of processes in the middle of a C
method, we do the following (similar to [
An example for method suspension is shown in Listing 1.2. In Line 3, the
process is put to sleep. To actually suspend method execution, local variables and
the return label are saved in Line 5, 6 and 8. The method is left in Line 9. The
process can resume execution at the point where it was suspended by jumping
to the return label de ned in Line 11. Then, local variables are restored and
execution is continued.
Method Call Transformation A further challenge when modeling process
suspension that a process may be not necessarily in the method that is directly bound
to the process, it may also be in any method of its call stack. In [
An example for a method call with process suspension is shown in Listing 1.3. Note that local variables have to be saved before the method call (Line 4), and also adding a return label and restoring of local variables have to be done before the method is called (Line 6) to cope with the case where the called method already was suspended and has to be called again. After the method call (Line 8), the check whether it was suspended is performed and, if necessary, the return label to execute the method call again is saved and the outer method is suspended as well (Line 10 to 13). 5
We have implemented the transformation from SystemC to the input language
of BLAST as described above in Java. To show the practical applicability of our
approach and to compare it with our previous approach where SystemC designs
are translated into UPPAAL timed automata [
In our experiments, we checked that a wheel slip always triggers the anti-slip regulation (ASR) and that a wheel lock always triggers the anti-lock braking system (ABS). Both properties can be speci ed as reachability properties as shown in Listing 1.4.
The BLAST model checker automatically checks for reachability of the
ERROR label, which in this case is unreachable. This proves that the ASR is always
triggered if a wheel slip is detected. The veri cation times are shown in Table 1.
The veri cation of the ASR took approximately 7 minutes, the veri cation of
the ABS approximately 8 minutes. As shown in [
In future work, we plan to combine our previous work, where the UPPAAL model checker is used for veri cation, with our novel approach for the veri cation of SystemC designs using the BLAST model checker. We think that the former is better suited for systems or subsystems where time, concurrency and communication play the most important role while the latter is better suited for systems or subsystems where data handling predominates.