DocumentCode :
2350726
Title :
Towards formal verification of analog designs
Author :
Gupta, Swastik ; Krogh, Bruce H. ; Rutenbar, Rob A.
Author_Institution :
Dept. of Electr. & Comput. Eng., Carnegie Mellon Univ., Pittsburgh, PA, USA
fYear :
2004
fDate :
7-11 Nov. 2004
Firstpage :
210
Lastpage :
217
Abstract :
We show how model checking methods developed for hybrid dynamic systems may be usefully applied for analog circuit verification. Finite-state abstractions of the continuous analog behavior are automatically constructed using polyhedral outer approximations to the flows of the underlying continuous differential and difference equations. In contrast to previous approaches, we do not discretize the entire continuous state space, and our abstraction captures the relevant behaviors for verification in terms of the transitions between "states" (regions of the continuous state space) as a finite state machine in the hybrid system model. The approach is illustrated for two circuits, a standard oscillator benchmark, and a much larger and more realistic delta-sigma (AI) modulator.
Keywords :
analogue circuits; finite state machines; formal verification; oscillators; sigma-delta modulation; state-space methods; analog circuit verification; analog designs; continuous state space; delta-sigma modulator; difference equations; differential equations; finite state machine; finite-state abstractions; formal verification; hybrid dynamic systems; model checking methods; polyhedral outer approximations; standard oscillator benchmark; Analog circuits; Analog computers; Circuit simulation; Circuit synthesis; Equations; Formal verification; Mathematical model; Oscillators; Power system modeling; State-space methods;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Computer Aided Design, 2004. ICCAD-2004. IEEE/ACM International Conference on
ISSN :
1092-3152
Print_ISBN :
0-7803-8702-3
Type :
conf
DOI :
10.1109/ICCAD.2004.1382573
Filename :
1382573
Link To Document :
بازگشت