Requirements and concepts for transaction level assertion refinement

Both hardware design and verification methodologies show a trend towards abstraction levels higher than RTL, referred to as transaction level (TL). Transaction level models (TLMs) are mostly used for early prototyping and as reference models for the verification of the derived RTL designs. Assertion based verification (ABV), a well known methodology for RTL models, has started to be applied on TL as well. The reuse of existing TL assertions for RTL and/or mixed level designs will especially aid in ensuring the functional equivalence of a reference TLM and the corresponding RTL design. Since the underlying synchronization paradigms of TL and RTL differ - transaction events for TL, clock signals for RTL - a direct reuse of these assertions is not possible. Currently there is no established methodology for refining the abstraction of assertions from TL towards RTL. In this paper we discuss the problems arising when refining TL assertions towards RTL, and derive basic requirements for a systematic refinement methodology. Building on top of an existing assertion language, we discuss some additional features for the refinement process, as well as some examples to clarify the steps involved.