Publications of Matthieu Moy in 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 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.

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.

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.