A formal approach to nonlinear analog circuit verification

ABSTRACT

This contribution presents an approach to nonlinear dynamic analog circuit verification. The input-output behavior of two systems is analyzed to check whether they are functionally similar. The algorithm compares the implicit nonlinear state space descriptions of the two systems on the same or on different levels of abstraction by sampling the state spaces and by building a nonlinear one-to-one mapping of the state spaces. Some examples demonstrate the feasibility of our approach.

REFERENCES

• 1: F.H. Bursal, B. H. Tongue, "A New Method of Nonlinear System Identification Using Interpolated Cell Mapping"; Proc. of the American Control Conf., Vol 4, pp. 3160-4, 1992
• 2: L. Fortuna, G. Nunnari and A. Gallo, "Model Order Reduction Techniques with Applications in Electrical Engineering", Springer-Verlag London, 1992
• 3: M.C. McFarland, "Formal Verification of Sequential Hardware: A Tutorial", IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 12, No. 5, May 1993
• 4: Wolfgang Mathis, Geometric Theory of Nonlinear Dynamical Networks, Proceedings of the A Selection of Papers from the Second International Workshop on Computer Aided Systems Theory, p.52-65, April 15-19, 1991
• 5: W. Mathis, "Theorie nichtlinearer Netzwerke" (in german); Springer Verlag, Berlin, 1987,
• 6: Maple VTM, Waterloo Maple Software, University of Waterloo, Version 5.2, 1994
• 7: P.E. Gill, W. Murray, M.H. Wright, "Practical Optimization", Academic Press Inc., London, 1981

INDEX TERMS

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

Additional Classification:
  J. Computer Applications

General Terms:
Algorithms, Theory

Keywords:
electronic design automation, analog nonlinear circuits, functional verification, formal verification, behavioral description