A Temporal Language for SystemC

We describe a general approach for defining new temporal specification languages, and adopting existing languages, for SystemC. We define the concept of "underlying trace" describing the execution of a SystemC model, and then define a set of important primitive assertions about the states in the trace. Our framework not only provides additional expressive power for making atomic assertions, but also provides very fine control over the temporal resolution of the language. Using the primitives defined here as clock expression allows sampling at different levels, from transaction-level to the level of individual statements. The advantage of our approach is that it defines important SystemC properties that have been overlooked previously, and also provides a uniform mechanism for specifying the sampling rate of temporal languages.

• Type: Conference
• Year: 2008
• Where: FMCAD
• Authors: Deian Tabakov, Gila Kamhi, Moshe Y. Vardi, Eli Singerman
• Keywords: FMCAD 2008, Formal Methods, Important Primitive Assertions, Systemc Model, Temporal Specification Languages