License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.09461.2
URN: urn:nbn:de:0030-drops-25102
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2510/
Go to the corresponding Portal

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

Formal Verification of Abstract SystemC Models

pdf-format:
09461.GrosseDaniel.Paper.2510.pdf (0.1 MB)

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:DagSemProc.09461.2,
  author =	{Grosse, Daniel and Le, Hoang M. and Drechsler, Rolf},
  title =	{{Formal Verification of Abstract SystemC Models}},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9461},
  editor =	{Bernd Becker and Valeria Bertacoo and Rolf Drechsler and Masahiro Fujita},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2010/2510},
  URN =		{urn:nbn:de:0030-drops-25102},
  doi =		{10.4230/DagSemProc.09461.2},
  annote =	{Keywords: SystemC, TLM, BMC, SAT, SMT}
}

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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI