A verification system for transient response of analog circuits using model checking

Conventional temporal logics like CTL (Clarke et al., 2000), used for specifying properties of digital systems are not well suited for property specification of analog systems. We present a new temporal logic for specifying properties of analog circuits. We call this logic Ana CTL (CTL for analog circuit verification). It is shown that Ana CTL is more suitable for specifying properties of analog systems than other temporal logics. The application of Ana CTL for verification of transient behavior of arbitrarily nonlinear analog circuits has been presented. The transient response of a circuit under all possible input waveforms is represented as a finite state machine (FSM), by bounding and discretizing the continuous state space of an analog circuit This FSM is created by means of repeated SPICE simulations. Algorithms have been developed to run Ana CTL queries on this discretized model. The structure of this FSM is well suited to represent the characteristics of analog circuits, and enables us to run complex queries including real-time constraints in polynomial time. The application of these methods on several real life analog circuits has been presented and we show that this system is a useful aid for detecting and debugging design errors.