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!  New

  • 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) New
    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) New
    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) New
    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