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.
Property Refinement