Grande Salle de VERIMAG
19 mars 2010 - 10h00
Static Analysis for SystemC with Scoot: From Verification to Simulation
par Nicolas Blanc de ETH Zurich
Abstract: SYSTEMC is a description language for computer systems that is based on C++.
The language is used for modeling electronic devices at arbitrary
levels of abstraction.
In particular, SystemC can describe models with both hardware and
software aspects.
As today’s electronic designs are incredibly large and complex,
validation of new products remains
time consuming as ever; hence the need to keep improving
state-of-the-art verification techniques.
We describe verification solutions for SystemC to improve reliability
of computer devices by
combining formal reasoning and simulation at high-level of abstraction.
In particular, our research indicates that formal methods have
applications beyond property checking,
namely for code optimizations, simulation, and testing. We show that
verification engines can be integrated
into compilation flows to compute information valuable at runtime,
statically. More specifically, our results
demonstrate that an application of formal engines at high abstraction
level is practical provided that:
1. the system is partitioned into “small” and independent verification
tasks, as monolithic approaches are
more subject to scalability issues,
2. the procedure takes advantage of today’s parallel computers to
distribute those tasks among many cores and
3. authorizes trading precision for time: It is often preferable to
provide partial results rapidly instead of complete
results after a long period of time.
We investigate solutions for the analysis of systems with hardware and
software components, exploring
how formal methods, classic static analysis techniques, and simulation
can be combined to improve state-of-the-art
verification. We have implemented these techniques in a compiler
prototype for the analysis of SystemC designs called
SCOOT. Given a SystemC model written in C++, SCOOT statically extracts
the module hierarchy and
generates a model in an intermediate representation that is suitable
for formal verification and simulation.
SCOOT is the first compiler for SystemC that uses formal methods to
improve simulation performance and coverage.
In particular, experimental evaluation indicates that SCOOT can
significantly speedup the execution of models
relevant for industry.
