Embedded System Design Topics, Techniques and Trends

Early prototyping with the usage of higher abstraction levels than RTL has
become increasingly popular during recent years [4] and is used more and more
in industrial workflows. The most common modeling paradigm in this regard
is transaction level modeling. Transaction Level models (TLMs) are used for
architecture exploration, as early platforms for software development, and later
on as golden reference models for verification of the corresponding RTL designs.
Besides, using so called transactors which translate TL protocols to RTL
and back, an existing TL model can also be used for testing an RTL component
in a TL environment without the need for the whole system to be implemented
in RTL already. First steps have been taken to apply Assertion Based Verification
(ABV), which has been successfully used for RTL verification for years, to
TLMs as well. Some of these attempts try to enhance existing approaches like
SystemVerilog Assertions (SVA) [1][11] or the Property Specification Language
(PSL) [8] in order to support TL designs and paradigms. In order to
really use TLMs as golden reference, a full equivalence check between TLM
and RTL would be desirable. One possibility to enhance the current state of the
art would be to reuse existing TL assertions for the RTL design or mixed level
designs. The main problem for this reuse attempt is based on the totally different
synchronization methods in TLM and RTL. On RTL all synchronization is
based on dedicated clock signals. In TL it is obtained by mutual dependencies
of transactions and potentially by the use of time annotations in addition to the
use of non-periodic trigger signals. Furthermore, the applied synchronization
schemes differ on the various TL sublevels. Since a reuse of TL assertions
for RTL and especially mixed level assertions has to support all synchronization
schemes involved, we chose to develop our own assertion language [6][7].
As with every refinement process, e.g. synthesis, this assertion refinement requires additional information and thus can never be fully automated. A partial
automation is possible by providing refinement related information upfront in
order to avoid the necessity for user interaction. This automated refinement
decreases time for rewriting assertions and guarantees a higher degree of consistency.
In this paper we discuss which additional information is necessary
for the refinement and how the process could be simplified and automated.
The paper is structured as follows. After discussing related work we give an
overview of the used assertion language. Afterwards we discuss some requirements
and useful features for the mixed level assertions followed by a small
example. As a next step we describe a methodical refinement process from TL
to RTL.We illustrate the assertion refinement by an application example which
also demonstrates the usefulness of the proposed features. After a summary we
give an outline of ongoing work towards packaging of assertions in a SPIRIT
conformal way.