Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Grosse, Daniel; Le, Hoang M.; Drechsler, Rolf License
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-25102

; ;

Formal Verification of Abstract SystemC Models



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

  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 =		{},
  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: 2010

DROPS-Home | Fulltext Search | Imprint Published by LZI