@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib matthieu_moy.bib -c year=2005 -ob 2005.bib}}
@inproceedings{lussy,
author = {Matthieu Moy and Florence Maraninchi and Laurent Maillet-Contoz},
title = {{LusSy}: A Toolbox for the Analysis of Systems-on-a-Chip at the Transactional Level},
booktitle = {International Conference on Application of Concurrency to System Design},
year = 2005,
month = {June},
url = {http://www-verimag.imag.fr/~moy/publications/acsd05.pdf},
pages = {26--35},
abstract = {We describe a toolbox for the analysis of Systems-on-a-chip
described in {SystemC} at the transactional level. The tools are able
to extract information from {SystemC} code, and to build a set of
parallel automata that capture the semantics of a {SystemC} design,
including the transaction-level specific constructs. As far as we
know, this provides the first executable formal semantics of
{SystemC}. Being implemented as a traditional compiler front-end, it
is able to deal with general {SystemC} designs. The intermediate
representation is now connected to existing formal verification
tools via appropriate encodings. The toolbox is open and other
tools will be used in the future.},
note = {Acceptance rate: 23/45 = 51\%}
}
@inproceedings{pinapa,
author = {Matthieu Moy and Florence Maraninchi and Laurent Maillet-Contoz},
title = {{Pinapa}: An Extraction Tool for {SystemC} descriptions of Systems-on-a-Chip},
booktitle = {EMSOFT},
year = 2005,
month = {September},
url = {http://www-verimag.imag.fr/~moy/publications/sc-compil.pdf},
code = {http://greensocs.sourceforge.net/pinapa/},
pages = {317--324},
abstract = {{SystemC} is becoming a de-facto standard for the description of
complex systems-on-a-chip. It enables system-level descriptions of
SoCs: the same language is used for the description of the
architecture, software and hardware parts.
A tool like pinapa is compulsory to work on realistic SoCs designs
for anything else than simulation: it is able to extract both
architecture and behavior information from {SystemC} code, with very
few limitations. pinapa can be used as a front-end for various
analysis tools, ranging from ``superlint'' to model-checking. It is
open source and available from
http://greensocs.sourceforge.net/pinapa/. There exists no equivalent
tool for {SystemC} up to now.},
note = {25/88 = 28\% accepted as regular papers, Rank A CORE 2014}
}
@incollection{tlm-book-chap5,
author = {Matthieu Moy},
title = {Chapter 5.9, Formal Verification},
booktitle = {Transaction-Level Modeling with {SystemC}. {TLM} Concepts and Applications for Embedded Systems},
pages = {190--206},
publisher = {Springer},
year = 2005,
editor = {Frank Ghenassia},
url = {http://www.springer.com/engineering/electronics/book/978-0-387-26232-1}
}
@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},
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.
}
}
@online{pinapa-software,
author = {Matthieu Moy},
title = {{Pinapa}: {P}inapa {I}s {N}ot a {P}arser},
howpublished = {Published as Free Software (LGPL License)},
year = 2005,
url = {http://greensocs.sourceforge.net/pinapa/}
}
This file was generated by bibtex2html 1.98.