License
When quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-25102
URL: http://drops.dagstuhl.de/opus/volltexte/2010/2510/
Go to the corresponding Portal

Grosse, Daniel ; Le, Hoang M. ; Drechsler, Rolf

Formal Verification of Abstract SystemC Models

pdf-format:
Document 1.pdf (105 KB)

Abstract

In this paper we present a formal verification approach for abstract SystemC models. The approach allows checking expressive properties and lifts induction known from bounded model checking to a higher level, to cope with the large state space of abstract SystemC programs. The technique is tightly integrated with our SystemC to C transformation and generation of monitoring logic to form a complete and efficient method. Properties specifying both hardware and software aspects, e.g. pre- and post-conditions as well as temporal relations of transactions and events, can be specified. As shown by experiments modern proof techniques allow verifying important non-trivial behavior. Moreover, our inductive technique gives significant speed-ups in comparison to simple methods.

BibTeX - Entry

@InProceedings{grosse_et_al:DSP:2010:2510,
  author =	{Daniel Grosse and Hoang M. Le and Rolf Drechsler},
  title =	{Formal Verification of Abstract SystemC Models},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  year =	{2010},
  editor =	{Bernd Becker and Valeria Bertacoo and Rolf Drechsler and Masahiro Fujita},
  number =	{09461},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2510},
  annote =	{Keywords: SystemC, TLM, BMC, SAT, SMT}
}

Keywords: SystemC, TLM, BMC, SAT, SMT
Seminar: 09461 - Algorithms and Applications for Next Generation SAT Solvers
Issue Date: 2010
Date of publication: 17.03.2010

DROPS-Home | Fulltext Search | Imprint Published by LZI