The project intends to build an experimental platform for validating
the correctness of analog and mixed-signal circuits, a component of
increasing importance for the functioning of modern embedded system.
The platform will combine two technologies currently being developed by
the partners: an effcient and physically-accurate simulator for large
analog and mixed-signal circuits and the methods for covering the state
space of such circuits by choosing appropriate input signals. The
project will be composed of the following three activities:
- Development of search-based methods for validating
large-scale continuous and hybrid systems
- Development of numerical analysis techniques for non-smooth
- Tool development (including generation of circuit equations
from models, optimization, etc.) and application to circuit benchmarks.
Principal work packages
Coverage guided simulation.
In order to measure simulation quality, we define coverage criteria
that reflect the properties to verify. These criteria are then used to
guide the simulation, which enables us to guarantee some coverage and
convergence (in comparison with exhaustive verification). This work
will build upon a coverage guided simulation method for continuous and
hybrid systems, which is being developed in VERIMAG. The method is inspired
by the probabilistic path and motion planning methods in robotics and
inherits their completeness properties.
Verification by simulation.
The existence of metrics on the system state space, which is natural
for continuous and hybrid systems, allows us to capitalize on the
recently developed concept of bisimulation metrics and infer all the
possible behaviors of the system in a neighborhood of a simulated
trajectory. Hence, by a finite number of simulations one can produce
results as strong as those obtained by exhaustive verification, such as
deciding whether the system is correct under all possible disturbances.
These bisimulation metrics can be used to define strategies for
exploration of the space of trajectories as well as for counter-example
guided refinement. Several strategies will be proposed and their
(theoretical and experimental) performance in verifying di erent types
of properties, such as those expressed in timed temporal logics, will
be analyzed. Also, a part of our work will aim at proposing necessary
algorithmic approaches to the computation of these bisimulation
Advanced numerical analysis techniques.
A performant simulation tool must rely on e cient and accurate
techniques for resolving circuit equations. The state-of-the-art SPICE
simulator is prone to convergence problems when the dynamics of the
circuit has fast variations caused by components with stiff
characteristics. Within this project, the INRIA-BIPOP team will address
these problems with a special set of models and dedicated algorithms
known as the non-smooth approach. Its application to the simulation of
mechanical systems has already been proved successful, and the goal of
this work package is to adapt this technology to electrical systems.
This adaptation involves, on one hand, the resolution techniques
specific to the circuit dynamics and, on the other hand, an optimal
extraction of the circuit equations in a required form from the
commonly-used description formalisms such as netlists. The techniques
and tools developed in this work package will serve as the computation
engine, on top of which the methods developed in the work packages WP1 and WP2 are used
to guide the simulation process.
development and application to analog and mixed signal circuit
The motivation for choosing this new but increasingly important
application domain is that on one hand these circuits can be naturally
modeled using hybrid systems and, on the other hand, we believe that
the new simulation tools developed in the context of the project will
contribute to enhance the automatization and reliability of the design
of analog and mixed-signal circuits. The goal of this work package is
to integrate all the results and tools obtained in the work packages WP1, WP2, and WP3 into a
tool box with a user-friendly graphical interface. The tool box will
then be tested on various benchmarks of analog and mixed signal