Towards formal verification of analog designs

Smriti Gupta, Bruce H. Krogh, Robin A Rutenbar

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 (ΔΣ) modulator.

Original languageEnglish (US)
Title of host publicationICCAD-2004 - IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers
Pages210-217
Number of pages8
DOIs
StatePublished - Dec 1 2004
EventICCAD-2004 - IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers - San Jose, CA, United States
Duration: Nov 7 2004Nov 11 2004

Publication series

NameIEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
ISSN (Print)1092-3152

Other

OtherICCAD-2004 - IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers
CountryUnited States
CitySan Jose, CA
Period11/7/0411/11/04

ASJC Scopus subject areas

  • Software
  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design

Fingerprint Dive into the research topics of 'Towards formal verification of analog designs'. Together they form a unique fingerprint.

Cite this