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 :
بازگشت