Scoot

A Tool for the Static Analysis of SystemC

Description

SCOOT statically analyses systems described using SystemC and ex­tracts 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. SCOOT produces then a simulator for the systematic exploration of the behaviors of the system.

Contact Nicolas Blanc with questions about SCOOT or feedback.

Installation

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 com­parison 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

Simulation Speedup

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:
cd examples/aes128lowarea

The benchmark encrypts and decrypts 128-bits numbers for 5*10⁶ 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:
make systemc_sim

Similarly, the next command creates the SCOOT simulator:
make scoot_sim

Finally, these last commands run the binaries and print execution-time statistics:
time ./systemc_sim
time ./scoot_sim

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.

Previous Versions

• scoot-oct-28-2009.tgz
• scoot-jun-11-2009.tgz
• scoot-mar-23-2009.tgz
• scoot-nov-2-2008.tgz
• scoot-jan-23-2008.tar.gz
• scoot-jan-18-2008.tar.gz
• scoot-dec-18-2007.tar.gz
• scoot-nov-2007.tar.gz
• scoot-ra-jul-29-2008.tar.gz
• scoot-ra-apr-7-2008.tar.gz

Publications and Presentations

• Static Analysis for SystemC with Scoot: From Verification to Simulation
  Technical Report
  Oct 2009.
• Fast Simulation of SystemC Designs with Scoot
  Institute Seminar at the Computer-System Departement of ETHZ,
  Oct 2009.
• Race Analysis for SystemC using Model Checking
  Blanc Nicolas, Kroening Daniel
  In Proceedings of ICCAD 2008 .
  (slides)
• Scoot: A Tool for the Analysis of SystemC Models
  Blanc Nicolas, Kroening Daniel, and Sharygina Natasha
  In Proceedings of TACAS 2008 Springer, 2008.
  (slides)