Towards Automated Refinement of TLM Properties to RTL

Abstract

In the recent years, the emergence of the Electronic System Level (ESL) can be witnessed. An ESL design flow starts with a TLM description, which is thoroughly verified and then refined to a RTL description in subsequent steps. Obviously, the correctness of TLM models is of great importance, as undetected errors will propagate and become very costly. In the past few years, a wide body of verification techniques at TLM has been developed ranging from simulation- based to formal verification, which typically employs property checking. The subsequent verification of the RTL model is commonly performed by a TLM/RTL co-simulation, where the same input stimuli are applied to both models and their outputs are checked for equivalence. This step requires an additional executable verification component, known as transactor, to bridge the function calls at TLM with the signal-based interfaces at RTL and vice versa. Due to incompleteness, it is highly desirable that co-simulation is complemented with other (preferably formal) approaches. A promising direction is to reuse properties that have been proven on the TLM model. However, semantic differences of the involved abstraction levels prevent straight-forward reuse. The translation process, i.e. TLM-to-RTL property refinement, is mostly manual, therefore error-prone and time-consuming. To the best of our knowledge, we propose in this paper the first fully automated TLM-to- RTL property refinement approach [1]. The main idea lies in a better reuse of the readily available transactors. At the core of our approach is a static transactor analysis based on symbolic execution. Essentially, the analysis reverse-engineers the executable transactors to create a formal specification of the underlying protocol as Finite State Machines (FSM). Starting with the initial symbolic execution state, the transactor function is repeatedly executed, until all reachable states are explored. This symbolic state space is transformed into an FSM by abstracting away all data except the RTL signal values. Then, TLM properties are refined by relating high-level TLM events with RTL signal combinations at different clock cycles based on the FSM. As a feasibility study we applied our refinement approach on a realistic case study of an ATM receiver device with two representative TLM properties. We believe that the proposed approach is of great practical interest. For future work we plan to define a formal characterization of supported properties.