Embedded System Design Topics,

Early prototyping with the usage of higher abstracTIon levels than RTL hasbecome increasingly popular during recent years [4] and is used more and morein industrial workflows. The most common modeling paradigm in this regardis transacTIon level modeling. TransacTIon Level models (TLMs) are used forarchitecture exploraTIon, as early platforms for software development, and lateron as golden reference models for verification of the corresponding RTL designs.Besides, using so called transactors which translate TL protocols to RTLand back, an existing TL model can also be used for testing an RTL componentin a TL environment without the need for the whole system to be implementedin RTL already. First steps have been taken to apply Assertion Based Verification(ABV), which has been successfully used for RTL verification for years, toTLMs as well. Some of these attempts try to enhance existing approaches likeSystemVerilog Assertions (SVA) [1][11] or the Property Specification Language(PSL) [8] in order to support TL designs and paradigms. In order toreally use TLMs as golden reference, a full equivalence check between TLMand RTL would be desirable. One possibility to enhance the current state of theart would be to reuse existing TL assertions for the RTL design or mixed leveldesigns. The main problem for this reuse attempt is based on the totally differentsynchronization methods in TLM and RTL. On RTL all synchronization isbased on dedicated clock signals. In TL it is obtained by mutual dependenciesof transactions and potentially by the use of time annotations in addition to theuse of non-periodic trigger signals. Furthermore, the applied synchronizationschemes differ on the various TL sublevels. Since a reuse of TL assertionsfor RTL and especially mixed level assertions has to support all synchronizationschemes involved, we chose to develop our own assertion language [6][7].As with every refinement process, e.g. synthesis, this assertion refinement requires additional information and thus can never be fully automated. A partialautomation is possible by providing refinement related information upfront inorder to avoid the necessity for user interaction. This automated refinementdecreases time for rewriting assertions and guarantees a higher degree of consistency.In this paper we discuss which additional information is necessaryfor the refinement and how the process could be simplified and automated.The paper is structured as follows. After discussing related work we give anoverview of the used assertion language. Afterwards we discuss some requirementsand useful features for the mixed level assertions followed by a smallexample. As a next step we describe a methodical refinement process from TLto RTL.We illustrate the assertion refinement by an application example whichalso demonstrates the usefulness of the proposed features. After a summary wegive an outline of ongoing work towards packaging of assertions in a SPIRITconformal way.