Verifying analog oscillator circuits using forward/backward abstraction refinement

Goran Frehse, Bruce H. Krogh, Rob A. Rutenbar

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

Abstract

Properties of analog circuits can be verified formally by partitioning the continuous state space and applying hybrid system verification techniques to the resulting abstraction. To verify properties of oscillator circuits, cyclic invariants need to be computed. Methods based on forward reachability have proven to be inefficient and in some cases inadequate in constructing these invariant sets. In this paper we propose a novel approach combining forward- and backward-reachability while iteratively refining partitions at each step. The technique can yield dramatic memory and runtime reductions. We illustrate the effectiveness by verifying, for the first time, the limit cycle oscillation behavior of a third-order model of a differential VCO circuit.

Original languageEnglish (US)
Title of host publicationProceedings - Design, Automation and Test in Europe, DATE'06
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Print)3981080114, 9783981080117
DOIs
StatePublished - 2006
EventDesign, Automation and Test in Europe, DATE'06 - Munich, Germany
Duration: Mar 6 2006Mar 10 2006

Publication series

NameProceedings -Design, Automation and Test in Europe, DATE
Volume1
ISSN (Print)1530-1591

Other

OtherDesign, Automation and Test in Europe, DATE'06
CountryGermany
CityMunich
Period3/6/063/10/06

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint Dive into the research topics of 'Verifying analog oscillator circuits using forward/backward abstraction refinement'. Together they form a unique fingerprint.

Cite this