Abstract: With the introduction of complex analog designs the need to verify the circuit behavior completely and efficiently cannot be overemphasized. Recognizing the limitation of circuit simulation to achieve this goal, we present a novel approach based on formal techniques developed for digital circuits. Given a transfer function (specification) and its implementation using operational amplifier macro circuits, we verify the correctness of the transient behavior of the implementation over all possible input waveforms. Transforming the specification and the extracted state equations of the implementation from the s-domain to the Z-domain facilitates a digital representation in terms of adders, multipliers and delay elements. These two digitized circuits are then compared using techniques for checking compatibility of states in finite state machines. An example that illustrates the technique is presented.