Logo Universität Bremen
LOGO AGRA | AG Rechnerarchitektur

Arbeitsgruppe Rechnerarchitektur / AGRA | Informatik | FB03 | Universität Bremen


SCIVER - SystemC Induction-based VERifier for Transaction Level Models


SCIVER is a formal property checker for SystemC TLM models. In addition to simple assertions, SCIVER allows the verification of high-level properties such as the effect of a transaction or that a transaction is only started after a certain event. Properties are specified using a variant of PSL with support for TLM primitives.

SCIVER translates the SystemC model together with the monitoring logic for the property to a C model. Then, a novel induction-based verification method is applied to the C model. This enables SCIVER not only to detect a property violation, but also to prove its absence.


SCIVER is no longer developed and maintained as a standalone tool. The main ideas will be integrated into SISSI.

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

Documentation & References

For the technical background on SCIVER and approaches using the techniques of SCIVER we refer to the following papers:

©2023 | AG Rechnerarchitektur | Kontakt | Impressum & Datenschutz