A Framework for Verification of Transaction Level Models in SystemC
Due to their increasing complexity, today's SoC (System on Chip) systems are subject to a variety of
faults (e.g., single-event upset, component crash, etc.), thereby their
verification a highly important task of such systems. However, verification is
a complex task in part due to the large scale of integration of SoC systems and different levels of abstraction provided by
modern system design languages such as {\em SystemC}.
To facilitate the verification of SoC systems, this
dissertation proposes an approach for verifying inter-component communication
protocols in SystemC Transaction Level Modeling (TLM) programs.
SystemC is a widely
accepted language and an IEEE standard. It includes a C++ library of
abstractions and a run-time kernel that simulates the specified system, thereby
enabling the early development of embedded software for the system that is
being designed. To enable and facilitate the communication of different components
in SystemC, the Open SystemC
Initiative (OSCI) has proposed an interoperability layer (on top of SystemC) that enables transaction-based interactions
between the components of a system, called {\it Transaction Level Modeling }
(TLM).
In order to verify SystemC TLM
programs, we propose a method that includes five main steps, namely {\bf
defining formal semantics}, {\bf model extraction}, {\bf fault modeling}, {\bf
model slicing}, and {\bf model checking}.
%
In order to extract a formal model from the given SystemC TLM program, first we need to specify the
requirements of developing a formal semantics that can capture the SystemC TLM programs while still benefiting from automation
techniques for verification and/or synthesis. Based on this intuition, we
utilize two model extraction approaches that consider the architecture of the
given program too.
In the first approach, we propose a set of transformation
rules that helps us to extract a Promela model from
the SystemC TLM program. In the second approach, we
discuss how to extract a timed automata model from the given program.
When we have the formal model, we model and inject several
types of faults into the formal models extracted from the SystemC
TLM programs. For injecting faults, we have developed a tool, called {\em UFIT}, that takes a formal model and a desirable fault
type, and injects the faults into the model accordingly.
%The overhead of the faults is
reasonable.
The models extracted from the SystemC
TLM program are usually very complex. Additionally, when we inject faults into
these models they become even more complex. Hence, we utilize a model slicing
technique to slice the models in the presence or absence of faults. We have
developed a tool, called {\em USlicer}
that takes a formal model along with a set of properties that needs to be
verified, and generate a sliced model based on the given properties. The
results show that verification time and the memory usage of the sliced version
of the model is significantly smaller than that of the original model.
Subsequently, in some cases where the verification of the original formal
models is not even possible, using our model slicing technique makes the
verification possible in a reasonable time and space.
We demonstrate the proposed approach using several SystemC transaction level case studies. In each case study,
we explain each step of our approach in detail and discuss the results and
improvements in each of them.
Paper:
Return to the publication list
Return to the Sandeep's home page