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
Link To Document