Symbolic Behavioral Model Generation and Formal
Verification of Analog Circuits
Date: July 19th (Friday)
Time: 09:10-09:40
Abstract
In this presentation two important tasks of analog circuit design are considered. First, a fully
automatic method for generating behavioral models for nonlinear analog circuits is presented. This
method is based on simplifications of the system of symbolic nonlinear differential equations
which is derived from a transistor level netlist. Generated models include nonlinear dynamic
behavior. They are composed of symbolic equations comprising circuit parameters. The main ideas
of the algorithm are demonstrated by an illustrative example. The second part deals with an
approach to nonlinear dynamic analog circuit verification. The input-output behavior of two
circuits is analyzed to check whether they are functionally similar. These circuits are described by
systems of nonlinear differential equations which are e.g. generated by the model generation
algorithm mentioned above. The verification method compares the implicit nonlinear state space
descriptions of the two systems of equations. Some examples are given to demonstrate the
feasibility of this approach. Finally, the significance of the presented algorithms is discussed with
respect to analog circuit design.
