A Tool for the Static Analysis of SystemC
SCOOT statically analyses systems described using SystemC and extracts models that can be
passed to verification tools such as SatAbs or CBMC. After
extraction, it also offers the possibility to re-synthesize C++ code that
does not rely on the SystemC library and that can be compiled with
g++ to produce a very fast simulator.
The emphasis of
SCOOT is the scheduling of the SystemC
threads. The SystemC standard permits the simulator to implement a deterministic
scheduling policy, which often hides concurrency flaws.
SCOOT can perform
a race analysis using model checking techniques. It computes commuativity predicates of the
processes using the model checking engines of Satabs and CBMC.
then a simulator for the systematic exploration of the behaviors of
Contact Nicolas Blanc
with questions about
SCOOT or feedback.
This file contains a compiled version of
SCOOTfor Linux and a collection of benchmarks.
Download the latest tarball of
SCOOT. Extract its content,
and edit the file 'common.mk'. Adapt the settings to your
environment. The original SystemC library is used for comparison only,
SCOOT works without it. The SystemC library
is available from www.systemc.org.
Contents of the Package
- bin/ : scoot binaries for linux
- include/ : include files for scoot
- examples/ : collection of ready-to-run examples
- examples-ra/ : collection of ready-to-run race-analysis examples
The next figure quantifies the simulation speedup obtained using
SCOOT compared to the original SystemC simulator on Oct. 17 2009.
The experiments were conducted on a 3Ghz Linux machine with g++ 4.2.4.
Example: 128-bits AES
Enter the subdirectory that contains the benchmark:
The benchmark encrypts and decrypts 128-bits numbers for 5*106 time units. The correctness of the algorithm is verified via an assertion that checks if the decryption yields the original value.
The following command builds the original SystemC simulator:
Similarly, the next command creates the
Finally, these last commands run the binaries
and print execution-time statistics:
The next screenshot shows the execution time of both the original SystemC simulator and the Scoot simulator. The experiment was conducted on a Linux machine equipped with a Intel Pentium 4 processor running at 3GHz.
Publications and Presentations
- Static Analysis for SystemC with Scoot: From Verification to Simulation
- Fast Simulation of SystemC Designs with Scoot
Institute Seminar at the Computer-System Departement of ETHZ,
- Race Analysis for SystemC using Model Checking
Blanc Nicolas, Kroening Daniel
In Proceedings of ICCAD 2008 .
- Scoot: A Tool for the
Analysis of SystemC Models
Blanc Nicolas, Kroening Daniel, and Sharygina Natasha
In Proceedings of TACAS 2008 Springer, 2008.