« back

SCIVER - SystemC Induction-based VERifier for Transaction Level Models

Description

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.

Download

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

Benchmarks

• First SCIVER benchmark set from February, 7th, 2012
  sciver-benchmarks-20120207.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 SCIVER and approaches using the techniques of SCIVER we refer to the following papers:

• Automatic TLM Fault Localization for SystemC (TCAD 2012)
• Towards Proving TLM Properties with Local Variables (CFV 2011)
• Automatic Fault Localization for SystemC TLM Designs (MTV 2010)
• Towards Analyzing Functional Coverage in SystemC TLM Property Checking (HLDVT2010)
• Proving Transaction and System-level Properties of Untimed SystemC TLM Designs (MEMOCODE 2010)