• DocumentCode
    1836152
  • Title

    Monitoring temporal SystemC properties

  • Author

    Tabakov, Deian ; Vardi, Moshe Y.

  • fYear
    2010
  • fDate
    26-28 July 2010
  • Firstpage
    123
  • Lastpage
    132
  • Abstract
    Monitoring temporal SystemC properties is crucial for the validation of functional and transaction-level models, yet the current SystemC standard provides no support for temporal specifications. In this work we describe a temporal monitoring framework for the SystemC specification language defined by Tabakov et al. at FMCAD´08. Our framework uses a very minimal modification of the SystemC kernel, exposing event notifications and simulation phases. The user code is instrumented to allow observation of the relevant parts of the model state. As proof of concept, we use the framework to specify and check properties of two SystemC models. We show that monitoring SystemC properties using this framework has reasonable overhead (0.01% - 1%) and has decreasing marginal cost. Finally, we demonstrate that monitoring at different levels of abstraction requires very small changes to the specification and the generated monitors. Based on our empirical results we argue that the additional expressive powers and flexibility of the framework does not incur a serious performance hit.
  • Keywords
    C++ language; formal verification; simulation languages; specification languages; SystemC kernel; SystemC specification language; temporal monitoring; transaction level model; Clocks; Kernel; Libraries; Monitoring; Object oriented modeling; Process control; Semantics;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Formal Methods and Models for Codesign (MEMOCODE), 2010 8th IEEE/ACM International Conference on
  • Conference_Location
    Grenoble
  • Print_ISBN
    978-1-4244-7885-9
  • Electronic_ISBN
    978-1-4244-7886-6
  • Type

    conf

  • DOI
    10.1109/MEMCOD.2010.5558640
  • Filename
    5558640