Execution semantics and formalisms for multi-abstraction TLM assertions

Electronic System Level (ESL) reflects the current trend in hardware design and verification towards abstraction levels higher than RTL, referred to as Transaction Level (TL). Raising the abstraction level leads to reduced complexity compared to classical RTL modeling; however, due to this lack of detail, verification of higher level models produces new problems. Assertion based verification (ABV) - a well established RTL methodology - is a good example of this. Temporal relations in RTL properties are specified in terms of clocks that trigger the design. It is not obvious how to specify properties for more abstract, non-clocked models where the notion of time is annotated as estimated delay values or omitted completely. Since ABV has already shown to be a strong methodology for functional RTL verification, we expect the same benefit for TL by lifting current ABV approaches to a higher level. In this paper we present a prototypic formal framework for specifying TL properties. We focus our work on three TL model views, as defined in the OSCITLM standard. For each view we describe the model of computation and derive the required operators. Furthermore, we explain the required execution semantics and give some application examples.