#
Research on Analog Circuit Verification at VERIMAG

This page
reports some preliminary research efforts toward the formal verification of analog and mixed-signal circuits in which our group
participated. Many of those took place within the European project PROSYD (property-based system design)
and other projects dedicated to the verification of continuous and
hybrid systems in general, that is, not necessarily systems that model
circuits.
Our work in this domain can be divided into two major directions. The
first is the definition of a language for describing properties of
analog signals (a basis for a future PSL-AMS) and deriving
automatically monitors, programs that can read simulation traces and
detect property violations. This work is, in principle, ready for industrial transfer. The other direction is the extension of verification
algorithms to deal with continuous variables and differential
equations. So far these techniques are restricted to very small circuits but we are working hard on scalability. The verfication is done using our tools d/dt ,
Phaver as well as other
ad-hoc prototypes. Below is an annotated list of reports and research
papers.

### Introductory Material

PROSYD deliverable D1.3/1 Extending PSL for Analog Circuits (2005)

This document includes a long introduction and historic survey of verification of discrete (digital) and continuous (analog) systems and the challenges that the latter pose

Analog Circuit Verification: a State of an Art (2005)

A preface to the proceeding of the first workshop on Formal Verification of Analog Circuits which is based on the introduction of deliverable D1.3/1

### Monitoring

ˇ
**The Analog Monitoring Tool (AMT) is available for download!**

O. Maler, D. Nickovic, **Monitoring Temporal Properties of
Continuous Signals** (2004)

Our first paper which defines STL (Signal Temporal Logic) as a formalism for describing certain types of properties of
analog signals. STL is based on the logic MITL for specifying
properties of Boolean signals. The paper has led to further
investigation of real-time logics and their monitoring which are outside the scope of this page

PROSYD deliverable 1.3/2 Final Proposal for Analog Extension to PSL (2007)

A final description of STL and some other metric-based operators. A bit verbose.

PROSYD deliverable 3.2/13 A Manual for the Analog Monitoring Tool (2007)

This tool translates automatically PSL properties into monitors that are connected to numerical simulators

PROSYD deliverable 3.2/2 Analog Case-Study (2007)

Demonstration of how the tool can be used to monitor properties of a FLASH memory

O. Maler, D. Nickovic, **AMT: a Property-based Monitoring Tool
for Analog Systems** (2007)

A recent paper which summarizes the logic, the tool and the case study. Slides

O. Maler, D. Nickovic, A. Pnueli, Checking Temporal Properties of Discrete, Timed and Continuous Behaviors (2007)

A paper summarizing the two monitoring algorithms and problems related to the analog signals.

K. Jones, V. Konrad and D. Nickovic, Analog Property Checkers: A DDR2 Case Study (2008)

Applying monitoring to part of the DDR standard.
### Verification of Small Circuits

T. Dang, A. Donze, O. Maler, ** Verification of Analog and Mixed Signal
Circuits using Hybrid Systems Techniques** (2004)

A paper reporting attempts to verify two small circuits, a biquad filter and a sigma-delta modulator using d/dt and HysDel, respectively

G. Frehse, B. Krogh, R. Rutenbar, O. Maler,** Time Domain Verification
of Oscillator Circuit Properties** (2006)

Specifying oscillator properties and applying Phaver to verify these properties on two oscillators

G. Frehse, B. Krogh, R. Rutenbar, ** **** Verifying Analog Oscillator Circuits Using Forward/Backward Abstraction ** (2006)

Continuation of the above.

E. M. Clarke, A. Donzé, A. Legay, **Statistical Model Checking of Mixed-analog Circuits with an application to a Third-order Delta-Sigma Modulator** (2008)

Verification of an analog circuit by sampling trajectories. slides

### Further Work

Here we mention some work on extedning the scope of continuous and analog verification, either by improved reachability computation or by systematic simulation with guaranteed coverage

E. Asarin, T. Dang, G. Frehse, A. Girard, C. Le Guernic, O. Maler,
**Recent Progress in Continuous and Hybrid Reachability Analysis** (2006)

A short summary of our recent progress, some described in the papers below

T. Dang
**Approximate Reachability Computation for Polynomial Systems** (2007)

How to extend reachability computation for non linear systems

A. Girard, C. Le Guernic, O. Maler,
** Efficient Computation of Reachable
Sets of Linear Time-Invariant Systems with Inputs** (2006)

How reachability computation can be performed for linear systems with hundreds of variables

T. Dang, T. Nahhal, **Randomized Simulation of Hybrid Systems
For Circuit Validation ** (2007)

Using guided random simulation for test coverage of continuous and hybrid systems

A. Donze, O. Maler,
**Systematic Simulation using Sensitivity Analysis** (2007)

Another way to sample the set of initial conditions of a continuous system in order to verify safety properties using finitely many simulations

### Useful Links

FAC'08 Formal Verification of Analog circuits Princeton, July 2008

**FAC'09** will be held as a satellite workshop for CAV'09 Grenoble, end of June 2009

Last update, 12/11/2008