2009, English, Article edition: Verification of an Industrial SystemC/TLM Model using LOTOS and CADP Garavel, Hubert; Helmstetter, Claude; Ponsini, Olivier; ...

User activity

Share to:
 
Bookmark: http://trove.nla.gov.au/version/202263
Physical Description
  • text
Published
  • HAL - CCSD
  • 2009
Language
  • English

Edition details

Title
  • Verification of an Industrial SystemC/​TLM Model using LOTOS and CADP
Author
  • Garavel, Hubert
  • Helmstetter, Claude
  • Ponsini, Olivier
  • Serwe, Wendelin
Published
  • HAL - CCSD
  • 2009
Physical Description
  • text
Subjects
Notes
  • SystemC/​TLM is a widely used standard for system level descriptions of complex architectures. It is particularly useful for fast simulation, thus allowing early development and testing of the targeted software. In general, formal verification of SystemC/​TLM relies on the translation of the complete model into a language accepted by a verification tool. In this paper, we present an approach to the validation of a SystemC/​TLM description by translation into LOTOS, reusing as much as possible of the original SystemC/​TLM C++ code. To this end, we exploit a feature offered by the formal verification toolbox CADP, namely the import of external C code in a LOTOS model. We report on experiments of our approach on the BDisp, a complex graphical processing unit designed by STMicroelectronics.
  • HAL:inria-00408283, version 1
  • HAL:http:/​/​hal.inria.fr/​inria-00408283/​en/​
Language
  • English
Contributed by
OAIster

Get this edition

  • Set up My libraries

    How do I set up "My libraries"?

    In order to set up a list of libraries that you have access to, you must first login or sign up. Then set up a personal list of libraries from your profile page by clicking on your user name at the top right of any screen.

  • All (1)
  • Unknown (1)
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.

User activity


e.g. test cricket, Perth (WA), "Parkes, Henry"

Separate different tags with a comma. To include a comma in your tag, surround the tag with double quotes.

Be the first to add a tag for this edition

Be the first to add this to a list

Comments and reviews

What are comments? Add a comment

No user comments or reviews for this version

Add a comment