Towards Equivalence Checking Between TLM and RTL Models

The always increasing complexity of digital system is overcome in design flows based on Transaction Level Modeling (TLM) by designing and verifying the system at difbstraction levels. The design implementation starts from a TLM high-level description and, following a topdown approach, it is refined towards a corresponding RTL model. However, the bottom-up approach is also adopted in the design flow when already existing RTL IPs are abstracted to be reused into the TLM system. In this context, proving the equivalence between a model and its rer abstracted version is still an open problem. In fact, traditional equivalence definitions and formal equivalence checking methodologies presented in the literature cannot be applied due to the very different internal characteristics of the models, including structure organization and timing. Targeting this topic, the paper presents a formal definition of equivalence based on events, and then, it shows how such a definition can be used for ...

• Type: Conference
• Year: 2007
• Where: MEMOCODE
• Authors: Nicola Bombieri, Franco Fummi, Graziano Pravadelli, João Marques-Silva
• Keywords: Corresponding Rtl Model, Design flow, MEMOCODE 2007, RTL IPs