Ph.D thesis of Computer Science: Techniques and Tools for the Verification of Systems-on-a-Chip at the Transaction Level

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.

Full document

The full document can be downloaded here: these-en.pdf.

Slides of the presentation

The slides presented on December 9th can be downloaded here: slides-these.pdf.


Details and BibTeX entries available here.

LusSy: A Toolbox for the Analysis of Systems-on-a-Chip at the Transactional Level

In proceedings of ACSD 2005

Pinapa: An Extraction Tool for SystemC descriptions of Systems-on-a-Chip

In proceedings of EMSOFT 2005

Formal verification section of the book: Transaction-Level Modeling with SystemC. TLM Concepts and Applications for Embedded Systems

Published by Springer

LusSy: an open Tool for the Analysis of Systems-on-a-Chip at the Transaction Level

In the journal Design Automation for Embedded Systems, 2006

Open-source release of Pinapa

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:

  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 =          "",
  month =     {December}

Works related to this Ph. D

Matthieu MOY
Back to home page
Last updated: December 14th 2007.