Towards Fully Automated TLM‐to‐RTL Property Refinement⋆
Vladimir Herdt1,a, Hoang M. Le1,b, Daniel Große1,2,c and Rolf Drechsler1,2,d
1Institute of Computer Science, University of Bremen, Bremen, Germany
avherdt@informatik.uni-bremen.de
bhle@informatik.uni-bremen.de
2Cyber-Physical Systems, DFKI GmbH, Bremen, Germany
cgrosse@informatik.uni-bremen.de
ddrechsle@informatik.uni-bremen.de
ABSTRACT
An ESL design flow starts with a TLM description, which is thoroughly verified and then refined to a RTL description in subsequent steps. The properties used for TLM verification are refined alongside the TLM description to serve as starting point for RTL property checking. However, a manual transformation of properties from TLM to RTL is error prone and time consuming. Therefore, in this paper we propose a fully automated TLM‐to‐RTL property refinement based on a symbolic analysis of transactors. We demonstrate the applicability of our property refinement approach using a case study.
