Automatic Equivalence Checking for SystemC-TLM 2.0 Models Against their Formal Specifications
Mehran Goli1,a, Jannis Stoppe1,2,b and Rolf Drechsler1,2,c
1Institute of Computer Science, University of Bremen, 28359 Bremen, Germany.
amehran@informatik.uni-bremen.de
bjstoppe@informatik.uni-bremen.de
cdrechsle@informatik.uni-bremen.de
2Cyber-Physical Systems, DFKI GmbH, 28359 Bremen, Germany
ABSTRACT
The necessity to handle the increasing complexity of digital circuits has led to the usage of more and more abstract design paradigms. In particular, the Electronic System Level (ESL) has become an area of active research and industrial application, especially via SystemC and its Transaction Level Modeling (TLM) framework. Additionally, the usage of formal specification languages such as the Unified Modeling Language (UML) prior to the implementation (even at higher abstraction levels) is now a broadly accepted workflow.
Utilizing this layered approach leaves the translation from the specification to the implementation to the designer, leaving the question unanswered how the equivalence of these should be verified. This paper proposes a novel, non-intrusive and broadly applicable approach to automatically validate the equivalence of the structural and behavioral information of a SystemC-TLM 2.0 model and its formal specification.
