Specification language for transaction level assertions

Transaction level (TL) modeling is the basis of the so called Electronic System Level that allows development of systems on chip at a quicker pace than with classical RTL approaches. Starting from the specification phase of the product development cycle, TL modeling enables easy architecture exploration and early software co-development. In contrast to RTL, TL models (TLM) are more abstract and do not contain micro-architectural details for instance; the design focus is on high-level control and data flow. Since TLMs are essential at the decision process in early system development and as they can serve as golden reference models for later RTL regression, it is imperative to ensure that they implement the specification correctly. Assertion Based Verification (ABV) has given a good return of investment in RTL verification, decreasing debug time while preserving the design intent. Leveraging these benefits on the transaction level for the verification of TLMs requires the adaptation of current ABV approaches to the specific characteristics of these abstract models. In this paper we present an assertion specification language, based on formal definitions, that allows the specification of transaction level properties and their execution in simulation. We derive the language from known ABV languages and extend these by the required TL functionality, and explain how simulation traces of finite length can be checked against properties.