Projects
People
Virtual prototyping consists in writing an executable model of a system before the actual system is available. Like many model-driven approaches, virtual prototyping involves a model of the system early in the design flow. However, a virtual prototype is not used to derive the final system, but only to validate some decisions on the system early in the design flow and develop embedded software early.
We focus on virtual prototyping of Systems-on-a-Chip (SoC), which we study in close partnership with STMicroelectronics since 2002. In the case of SoCs, virtual prototyping allows validating the architecture of the hardware system, developing the embedded software, and estimating power consumption and temperature. The standard for SoC modeling is Transaction-Level Modeling (TLM) in SystemC.
Analysis and Verification of SystemC Programs
The teem pioneered the work on dedicated compiler front-ends for SystemC/TLM programs with tools like Pinapa and PinaVM, used initially for formal verification (LusSy and PinaVM), and later for optimized compilation (Tweeto). We also developed run time-verification tools (SCRV) to explore exhaustively and efficiently all possible schedules.
Parallel and Distributed Executions of SystemC Programs
One of the current challenges both in research and industry is to allow parallel execution of SystemC/TLM programs. Indeed, SystemC programs are parallel in essence since they describe a hardware system, but their execution with the reference implementation of SystemC is sequential. Most parallel and distributed event simulation (PDES) approaches do not apply directly on loosely timed TLM programs.
We studied several approaches to relax the constraints imposed by simulated time and TLM communication, like sc-during, Samuel Jones and Yussef Bouzouzou’s tools. We are improving and extending these tools to apply them on large industrial case-studies.
Extra-Functional Properties
SystemC/TLM was designed to model the functional properties of a system, and to some extent, timing. We developed tools for co-simulation with other simulators (e.g. power and thermal solvers). We developed approaches to improve the faithfulness with respect to the final system and avoid simulation artifacts due to loose timing.
Contract-based Design and Verification
We also work on increasing the level of abstraction by using non-deterministic specifications. Non-determinism is used to model components for which the full specification is not yet available, or some level of uncertainty in the specification (e.g. when the exact timing or the exact order of events is not known, we can still specify a timing interval or a partial order). A non-deterministic specification can either be used for early simulation, before the deterministic implementation is available, or to check that a deterministic implementation is a refinement of the specification (defensive programming).
A non-deterministic specification is usually expressed as an Assume/Guarantee contract : the assume clause is a property that the environment must satisfy, and the Guarantee is a property that the system satisfies, provided the Assume clause is true.
We initially applied the contract-based design on functional specification, and are extending it to power and temperature.