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.
- First SCIVER benchmark set from February, 7th, 2012
Notification of updates
Please consider subscribing to our mailing list.
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)