@phdthesis{Moy05a,
title = { Techniques and Tools for the Verification of Systems-on-a-Chip at the Transaction Level },
author = {Moy, Matthieu},
month = {December},
year = {2005},
school = {INPG, Grenoble, France},
team = {SYNC},
abstract = {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 compositional verification tools, or static code analyzers 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.},
}
