Sciweavers

Share
ENTCS
2006

Time Domain Verification of Oscillator Circuit Properties

8 years 11 months ago
Time Domain Verification of Oscillator Circuit Properties
The application of formal methods to analog and mixed signal circuits requires efficient methods tructing 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 tunneldiode circuit model using PHAVer, a hybrid system analysis tool that provides sound verification results based on linear hybrid automata approximations and infinite precision computations.
Goran Frehse, Bruce H. Krogh, Rob A. Rutenbar, Ode
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Goran Frehse, Bruce H. Krogh, Rob A. Rutenbar, Oded Maler
Comments (0)
books