SystemC is a de-facto standard language for high-level modeling of systems on chip. We investigate the feasibility of explicit state model checking of SystemC programs, proposing several ways to convert SystemC into Promela. We analyze the expressiveness of the various encoding styles, and we experimentally evaluate their impact on the search carried out by SPIN on a significant set of benchmarks. We also compare the results with recent approaches to symbolic verification of SystemC. Our approach never returns false positives, detects assertion violations much faster than recent formal approaches, and has the novel feature of pinpointing non-progressing delta cycles.

An Analytic Evaluation of SystemC Encodings in Promela

Campana, Daniele;Cimatti, Alessandro;Narasamdya, Iman;Roveri, Marco
2011-01-01

Abstract

SystemC is a de-facto standard language for high-level modeling of systems on chip. We investigate the feasibility of explicit state model checking of SystemC programs, proposing several ways to convert SystemC into Promela. We analyze the expressiveness of the various encoding styles, and we experimentally evaluate their impact on the search carried out by SPIN on a significant set of benchmarks. We also compare the results with recent approaches to symbolic verification of SystemC. Our approach never returns false positives, detects assertion violations much faster than recent formal approaches, and has the novel feature of pinpointing non-progressing delta cycles.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/31959
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact