A practical approach for monitoring analog circuits

ABSTRACT

Formal methods have been advocated for the verification of digital design where correctness is proved mathematically. In contrast to digital designs, the verification of analog and mixed signal systems is a challenging task that requires lots of expertise and deep understanding of their behavior. In this paper, we present a run-time verification methodology based on monitoring the behavior (solution flow) of analog circuits. Monitors are deterministic timed automata that can be synthesized from temporal properties. For illustration purposes, we applied our methodology on the verification of the oscillation property of a tunnel diode oscillator.

REFERENCES

• 1: Rajeev Alur , Costas Courcoubetis , David Dill, Model-checking in dense real-time, Information and Computation, v.104 n.1, p.2-34, May 1993 [doi>10.1006/inco.1993.1024 ]
• 2: Ilan Beer , Shoham Ben-David , Cindy Eisner , Dana Fisman , Anna Gringauze , Yoav Rodeh, The Temporal Logic Sugar, Proceedings of the 13th International Conference on Computer Aided Verification, p.363-367, July 18-22, 2001
• 3: T. Dang, A. Donze, O.Maler. Verification of analog and mixed-signal circuits using hybrid system techniques. In Formal Methods in Computer-Aided Design, LNCS 3312, Springer: 14--17, 2004.
• 4: G. Frehse, B. Krogh, R. Rutenbar, O. Maler Time Domain Verification of Oscillator Circuit Properties, Workshop on Formal Verification of Analog Circuits, April 9th, 2005, Edinburgh, UK.
• 5: M. Geilen. An Improved On-The-Fly Tableau Construction for a Real-Time Temporal Logic. In Computer Aided Verification, LNCS 2725, Springer, 2003, pp. 394--406.
• 6: M.C.W. Geilen. Formal Techniques for Verification of Complex Real-time Systems, Ph.D. Thesis, Eindhoven University of Technology, 2002.
• 7: Mark R. Greenstreet , Ian Mitchell, Reachability Analysis Using Polygonal Projections, Proceedings of the Second International Workshop on Hybrid Systems: Computation and Control, p.103-116, March 29-31, 1999
• 8: S. Gupta , B. H. Krogh , R. A. Rutenbar, Towards formal verification of analog designs, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.210-217, November 07-11, 2004 [doi>10.1109/ICCAD.2004.1382573]
• 9: W. Hartong, R. Klausen, L. Hedrich. Formal Verification for Nonlinear Analog Systems: Approaches to Model and Equivalence Checking, In Advanced Formal Verification, Kluwer, 2004, pp. 205--245.
• 10: L. Hedrich , E. Barke, A formal approach to verification of linear analog circuits wth parameter tolerances, Proceedings of the conference on Design, automation and test in Europe, p.649-655, February 23-26, 1998, Le Palais des Congrés de Paris, France
• 11: Andreas Lemke , Lars Hedrich , Erich Barke, Analog circuit sizing based on formal methods using affine arithmetic, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.486-489, November 10-14, 2002, San Jose, California [doi>10.1145/774572.774643]
• 12: R. J. Lohner, Enclosing the solutions of ordinary initial and boundary value problems, in Computer Arithmetic: Scientific Computation and Programming Language, Wiley-Teubner Series in Computer Science, Stuttgart, 1987, pp.255--286.
• 13: R.P. Kurshan and K.L. McMillan. Analysis of digital circuits through symbolic reduction. IEEE Transaction on Computer-Aided Design 10:pp.1350--1371, 1991.
• 14: M. Maidi, The common fragment of CTL and LTL, Proceedings of the 41st Annual Symposium on Foundations of Computer Science, p.643, November 12-14, 2000
• 15: O. Maler, D. Nickovic, Amir Pnueli. Real Time Temporal Logic: Past, Present, Future. In International Conference on Formal Modelling and Analysis of Timed Systems, LNCS 3829, Springer, 2005, pp.2--16.
• 16: O. Maler, D. Nickovic. Monitoring Temporal Properties of Continuous Signals. In International Conference on Formal Modelling and Analysis of Timed System, LNCS 3253, Springer, 2004, pp.152--166.
• 17: Ramon E. Moore , Fritz Bierbaum, Methods and Applications of Interval Analysis (SIAM Studies in Applied and Numerical Mathematics) (Siam Studies in Applied Mathematics, 2.), Soc for Industrial & Applied Math, 1979
• 18: L. Tan, J. Kim, I. Lee. Testing and Monitoring Model-based Generated Program. In Proc. Run-time Verification, Electronic Notes in Theoretical Computer Science, 89(2), 2003.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids
          Subjects: Verification

General Terms:
Verification