A Complete Verification Chain for SystemC/TLM
Since the PhD of Matthieu Moy, defended at the end of 2005, the group works on a complete verification chain for SystemC/TLM designs. The idea is to perform model extraction from SystemC code, and then to connect to existing verification tools (our model-checker Lesar, SMV and nuSMV, SPIN, and abstract interpretation tools like NBac).
This is different from approaches in which SystemC/TLM models are re-engineered into formal models, to ease the connection to verification tools. In these approaches, the semantics of the SystemC scheduler is changed, and a lot of uncontrollable abstractions are performed. Other approaches based on automatic formal model extraction from real SystemC code include that of [9] and [10].
The main elements of our chain are:
- a front-end for SystemC, called Pinapa, described in [11], and available as an open-source project Pinapa;
- a formalism for the extraction of models from SystemC/TLM, called HPIOM, for heterogeneous Parallel Input-Output machines; systems are described by products of extended synchronous automata;
- the back-ends that connect to SMV, Lesar, etc., from HPIOM.
The full chain is operational, and serves as a proof-of-concept. In particular, Pinapa allows to take any SystemC model into account, which is not the case for other SystemC front-ends. It has been used successfully for industrial case-studies provided by STMicroelectronics.
The verification of a large system-on-a-chip model, taken as a whole, is outside the scope of state-of-the art verification tools. Consequently, we now work on abstractions, component-by-component verification methods, and alternative encodings.
As far as the front-end is concerned, we now look at the SSA (single-static-assignment) form produced by GCC, because previous experiments by the Espresso group at INRIA Rennes have proved that the SSA form can be translated quite naturally into a synchronous formalism. This is one of the research objectives of the FoToVP ANR project (2006-2009) coordinated by Verimag/Synchrone.
See also VERIMAG + STMicroelectronics common projects [2002...[ for other approaches to the formal validation of SoCs, including runtime verification.
