(This announcement is also available from
http://www-verimag.imag.fr/~maraninx/?breve11 )
Postdoctoral Research position in Verimag, Grenoble, France:
"Exploiting the Static Single Assignment form in a tool-chain
for the formal verification of Transaction-Level Models (TLM)
of Systems-on-a-Chip written in SystemC"
Context: Transaction-Level Modeling of Systems-on-a-Chip
The Register Transfer Level (RTL) used to be the entry point of the
design flow of hardware systems, including systems-on-a-chip (SoCs).
However, the simulation environments for such models do not scale up
well. Developing and debugging embedded software for these low level
models before getting the physical chip from the factory is no longer
possible at a reasonable cost. New abstraction levels, such as the
Transaction-Level Modeling, have emerged. The TLM approach uses a
component-based approach, in which hardware blocks are modules
communicating with so-called transactions. The TLM models are used for
early development of the embedded software, because the high level of
abstraction allows a fast simulation. This new abstraction level
requires that SoCs be described in some non-deterministic asynchronous
way, with new synchronization mechanisms, quite different from the
implicit synchronization of synchronous circuit descriptions.
SystemC is a C++ library used for the description of SoCs at different
levels of abstraction, from cycle accurate to purely functional
models. It comes with a simulation environment, and is becoming a de
facto standard. SystemC offers a set of primitives for the description
of parallel activities representing the physical parallelism of the
hardware blocks. The TLM level of abstraction can be described with
SystemC.
VERIMAG and STMicroelectronics Common Projects
VERIMAG and STMicroelectronics have been working together on
TLM-related problems since 2002. The main problems we are looking at
are the following:
- How to connect SystemC to formal verification tools; this relies on a
front-end for SystemC called PINAPA, and on a semantic extractor able to
transform abstract syntax trees of SystemC models into some format
suitable for model-checking or abstract interpretation tools. The
whole tool-chain is called LusSy.
- How to cover correctly the potential parallelism that is present in a
SystemC design, and that is supposed to represent faithfully the
physical parallelism of the hardware? Our tool relies on dynamic partial
order reduction techniques.
- How to define precisely the nature of the information that should be
present in pure functional models (also called TLM-PV, for
"programmer's view") and in timed models (also called TLM-PVT, for
"programmer's view + time")? How to construct a PVT model from a PV
one without modifying its functionality, as seen by the developer of
the embedded software?
- How to define precisely what a TLM component should be, be it written
in SystemC or not?
These questions are being addressed in several projects:
- OpenTLM is a project of the competitiveness pole MINALOGIC in Grenoble
- FoToVP (Formal Tools for the Virtual Prototyping of Embedded Systems)
is a French National Project
The LusSy Tool-Chain
The LusSy tool-chain (mentioned above) does a succession of
transformations on SystemC source code to generate the input format
for various model-checkers.
One of the components of this tool-chain is Pinapa, which is the
equivalent of a compiler front-end for a programming language, but
applied to SystemC (which is indeed a C++ library). Pinapa uses GCC to
analyze the C++ part of the code, but adds to the abstract syntax tree
(AST) information on dedicated SystemC constructs (like the platform's
architecture, which component is connected to whom, ...), thus
allowing the extraction of a formal semantics from a SystemC program.
In the meantime, some interesting works have been carried out (in
particular by INRIA Rennes, also known as IRISA, our partner in the
FoToVP project) on the use of SSA (for "Static Single Assignment") to
perform efficient proofs of imperative code. The SSA form is an
intermediate form widely used in compilers since it is the one on
which optimization algorithms works best. It has been shown that
natural and efficient transformations from SSA to proof engines exist.
Objectives of the Post-Doc
The subject proposed is to introduce the notion of SSA form into the
tool-chain LusSy, in particular in the component Pinapa, while
improving its flexibility and extensibility. Indeed, Pinapa extracts
an abstract syntax tree close to the source language. Applying formal
methods with this tree as a starting point is complex and not very
efficient. Introducing SSA in the tool would improve this point.
The goal of this post-doc would therefore be to explore the
possibilities of introducing an SSA form within Pinapa.
Technically, two ways are possible obtain SSA code from a C++
program: GCC 4.x, which uses an SSA form internally, and (probably
better), LLVM which uses SSA in its byte-code.
But the real problem is to identify the SystemC specific constructs,
which have already been broken down into simpler constructs in SSA
code. For example, when one analyses the code
port.write(42);
we can consider it as a "normal" C++ piece of code, that any C++
front-end can analyze, but Pinapa will recognize it as a SystemC
specific construct: it is a write operation on a port, and Pinapa
needs to know at least who is connected to this port.
Summary of expected work
We expect :
1- A method to match SSA code against SystemC constructs. This is the
central point of the work.
2- the definition of an intermediate format containing the useful
information on SystemC. This format must be usable as an entry for
verification tools
3- A prototype-tool which could become the next version of Pinapa.
The tool should be able to read SystemC code and to produce the
defined intermediate format.
Point 2 must be achieved in collaboration with a post-doctoral
researcher that is currently working on intermediate formats as inputs
for verification tools. In addition, we expect a student to work with
the candidate on technical solutions (LLVM, gcc, etc.) for point 3.
Required Skills
The ideal candidate should have a Ph.D degree in computer science,
combine solid theoretical background and software development skills,
and have some degree of autonomy. Good English speaking and writing
skills are required (French is not required). The candidate should be
able to work in a collaborative environment, with a strong commitment to
reaching research excellence and achieving assigned objectives.
In depth previous experience in the following areas is required:
- C++ (some knowledge of SystemC would be appreciated)
- Compilation (architecture of a compiler, SSA form. Knowledge of LLVM
would be appreciated).
- Formal languages
Terms of employment
A full-time position as a postdoctoral researcher for an initial
period of 12 months starting as soon as possible after February 1st,
2009. The position can be extended to 6 more months.
The salary will be min. 2500 EUR and max 3000 EUR gross per month
depending on qualifications and experience.
Application
Send a detailed CV, a list of publications, a list of referees (persons
that can recommend you), and a short letter explaining your motivations
for this position, by email to:
Florence.Maraninchi@imag.fr,Matthieu.Moy@imag.fr,kevin.marquet@imag.fr
Please include [POSTDOC SOC] in the subject of your mail, and only
attach PDF files.
Send your application as soon as possible, and no later than December
1st, 2008 |
登录
多谢支持 贵在坚持。。。
