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 different abstraction levels. The design implementation starts from a TLM high-level description and, following a top- down 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 refined or 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 proving the equivalence in the RTL vs. TLM context, without requiring timing or structural similarities between the modules to be compared. Finally, the paper presents a practical use of the proposed theory, by proving the correctness of a methodology that automatically abstracts RTL IPs towards TLM implementations.