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

Dastidar, Tathagato Rai ; Chakrabarti, P. P. (2005) A verification system for transient response of analog circuits using model checking IEEE Transactions on Very Large Scale Integration (VLSI) Systems . pp. 195-200. ISSN 1063-8210

Full text not available from this repository.

Official URL: http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arn...

Related URL: http://dx.doi.org/10.1109/ICVD.2005.38

Abstract

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.

Item Type:Article
Source:Copyright of this article belongs to Institute of Electrical and Electronic Engineers.
ID Code:5916
Deposited On:19 Oct 2010 10:13
Last Modified:20 May 2011 09:31

Repository Staff Only: item control page