Thesis by Matthieu Moy, started in October 2002, part of a joint project between Verimag and STMicroelectronics. It was presented and defended publicly on December 9th 2005.
The work presented in this document deals with the formal verification models of Systems-on-a-Chip at the transaction level (TLM). We present the transaction level and its variants, and remind how this new level of abstraction is today necessary in addition to the register transfer level (RTL) to accommodate the growing constraints of productivity and quality, and how it integrates in the design flow.
We present a new tool, called LusSy, that allows property-checking on transactional models written in SystemC. Its structure is similar to the one of a compiler: A front-end, PINAPA, that reads the source program, a semantic extractor, BISE, into our intermediate formalism HPIOM, a number of optimizations in the component BIRTH, and code generators for provers like LUSTRE and SMV.
LusSy has been designed to have as few limitation as possible regarding the way the input program is written. PINAPA uses a novel approach to extract the information from the SystemC program, and the semantic extraction implements several TLM constructs that have not been implemented in any other SystemC verification tool as of now. It doesn't require any manual annotation. The tool chain is completely automated.
LusSy is currently able to prove properties on small platforms. Its components are reusable to build other tools for static code analysis using techniques other than model-checking that can scale up more efficiently.
We present the theoretical principles for each step of the transformation, as well as our implementation. The results are given for small examples, and for a medium size case-study called EASY. Experimenting with LusSy allowed us to compare the various tools we used as provers, and to evaluate the effects of the optimizations we implemented.
The full document can be downloaded here: these-en.pdf.
The slides presented on December 9th can be downloaded here: slides-these.pdf.
Details and BibTeX entries available here.
In proceedings of ACSD 2005
In proceedings of EMSOFT 2005
Published by Springer
In the journal Design Automation for Embedded Systems, 2006
Pinapa, the front-end component of LusSy, is available on sourceforge.
The list of publications cited in this work is available here.
To cite this thesis:
@PhdThesis{these-moy,
author = {Matthieu Moy},
title = {Techniques and Tools for the Verification of
Systems-on-a-Chip at the Transaction Level},
school = {INPG, Grenoble, France},
year = 2005,
URL = "http://www-verimag.imag.fr/~moy/phd/",
month = {December}
}