Time Domain Verification of Oscillator Circuit Properties

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

Research output: Contribution to journalArticlepeer-review


The application of formal methods to analog and mixed signal circuits requires efficient methods for constructing abstractions of circuit behaviors. This paper concerns the verification of properties of oscillator circuits. Generic monitor automata are proposed to facilitate the application of hybrid system reachability computations to characterize time domain features of oscillatory behavior, such as bounds on the signal amplitude and jitter. The approach is illustrated for a nonlinear tunnel-diode circuit model using PHAVer, a hybrid system analysis tool that provides sound verification results based on linear hybrid automata approximations and infinite precision computations.

Original languageEnglish (US)
Pages (from-to)9-22
Number of pages14
JournalElectronic Notes in Theoretical Computer Science
Issue number3 SPEC. ISS.
StatePublished - Jun 20 2006
Externally publishedYes


  • analog circuits
  • hybrid automata
  • hybrid systems
  • oscillators
  • verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Time Domain Verification of Oscillator Circuit Properties'. Together they form a unique fingerprint.

Cite this