Auditorium (IMAG)
10 May 2017 - 09h00
High-Level Component-Based Models for Functional Verification of Systems-on-a-Chip (Phd Defense)
by Yuliia Romenska from Univ. Grenoble Alpes
Abstract: The work presented in this thesis deals with modeling, specification
and testing of models of Systems-on-a-Chip (SoCs) at the transaction
abstraction level and higher. SoCs are heterogeneous: they comprise
both hardware components and processors to execute embedded software,
which closely interacts with hardware. SystemC-based Transaction
Level Modeling (TLM) has been very successful in providing high-level
executable component-based models for SoCs, also called virtual
prototypes (VPs). These models can be used early in the design flow
for the development of the software and the validation of the actual
hardware. For SystemC/TLM virtual prototypes, Assertion-Based
Verification (ABV) allows property checking early in the design cycle,
helping to find bugs early in the model and to save time and effort
that are needed for their fixing. TL models can be over-constrained,
which means that they do not represent all the behaviors of the
hardware, and thus, do not allow detection of some malfunctions of the
prototype. Our contributions consist of two orthogonal and
complementary parts: On the one hand, we identify sources of
over-constraints in TL models appearing due to the order of
interactions between components, and propose a notion of
loose-ordering which allows to remove these over-constraints. On the
other hand, we propose a generalized stubbing mechanism which allows
the very early simulation with SystemC/TLM virtual prototypes.
We propose a set of patterns to capture loose-ordering properties, and
define a direct translation of these patterns into SystemC monitors.
Our generalized stubbing mechanism enables the early simulation with
SystemC/TLM virtual prototypes, in which some components are not
entirely determined on the values of the exchanged data, the order of
the interactions and/or the timing. Those components have very
abstract specifications only, in the form of constraints between
inputs and outputs. We show that essential synchronization problems
between components can be captured using our simulation with stubs.
The mechanism is generic; we focus only on key concepts, principles
and rules which make the stubbing mechanism implementable and
applicable for real, industrial case studies. Any specification
language satisfying our requirements (e.g., loose-orderings) can be
used to specify the components, i.e., it can be plugged in the
stubbing framework. We provide a proof of concept to demonstrate the
interest of using the simulation with stubs for very early detection
and localization of synchronization bugs of the design.
PhD Defense Committee:
Pr. Erika Abraham, RWTH Aachen University, Germany
Pr. Franco Fummi, Verona University, Italy
Pr. Laurence Pierre, Grenoble Alpes University, France
Dr. Kim Gruttner, Carl von Ossietzky University of Oldenburg, Germany
Dr. Laurent Maillet-Contoz, STMicroelectronics, France
