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 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 Transaction Level Modeling (TLM).In order to verify SystemC TLM programs, we propose a method that includes five main steps, namely defining formal semantics, model extraction, fault modeling, model slicing, and 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 UFIT, that takes a formal model and a desirable fault type, and injects the faults into the model accordingly.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 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.
Read
