« zurück

SISSI - SystemC Intermediate Verification Language and Symbolic Simulator

NEW: the Language Reference Manual for the IVL is available here Description

SystemC Intermediate Verification Language (IVL) enables the independent development of front-ends and back-ends for SystemC formal verification. It is compact, intuitive, readable but expressive enough to capture the behavior of SystemC designs.

SISSI (SystemC IVL Symbolic Simulator) is a back-end for the IVL. It combines symbolic execution (full input coverage) and Partial Order Reduction (efficient pruning of search space). SISSI is able to find assertion violations as well as general errors such as division by zero or memory access violation in a given IVL description.

Tools

The grammar and a parser for the IVL and a set of benchmarks are available to download: systemc-ivl-20170630.tar.gz.
Older archives: systemc-ivl-20130528.tar.gz.

Contact
Please contact Rolf Drechsler in case of questions and/or problems at drechsler@uni-bremen.de.

Documentation & References

For the technical background on the IVL and the symbolic simulator SISSI we refer to the following paper:

• Verifying SystemC using Intermediate Verification Language and Stateful Symbolic Simulation (TCAD 2018)
• Verifying SystemC using Stateful Symbolic Simulation (DAC 2015)
• Verifying SystemC using an Intermediate Verification Language and Symbolic Simulation (DAC 2013)

For recent advancements based on SISSI:

• Compiled Symbolic Simulation for SystemC (ICCAD 2016)
• ParCoSS: Efficient Parallelized Compiled Symbolic Simulation (CAV 2016)
• Towards Formal Verification of Real-World SystemC TLM Peripheral Models - A Case Study (DATE 2016)