Monitoring temporal SystemC properties

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%

• Type: Journal
• Year: 2010
• Where: MEMOCODE
• Authors: Deian Tabakov, Moshe Y. Vardi
• Keywords: Formal Methods, MEMOCODE 2010, SystemC, SystemC Properties, Temporal Systemc Properties