DocumentCode
1772895
Title
Verifying robust frequency domain properties of non linear oscillators using SMT
Author
Asad, Hafiz Ul ; Jones, Kevin D. ; Surre, Frederic
Author_Institution
City Univ. London, London, UK
fYear
2014
fDate
23-25 April 2014
Firstpage
306
Lastpage
309
Abstract
We present a novel mixed time and frequency domain approach to the formal verification of oscillators properties which are specified in the frequency domain. We use robust periodogram specification to specify the oscillator behaviour in the close vicinity of the limit cycle. Using SAT modulo ODE (SMO) for Bounded Model Checking (BMC) of the non-linear hybrid automata, we show that the oscillator hybrid timed traces satisfy frequency domain specifications.
Keywords
computability; formal verification; mixed analogue-digital integrated circuits; oscillators; SAT modulo ODE; SMT; bounded model checking; formal verification; mixed time and frequency domain; non linear oscillators; non-linear hybrid automata; robust frequency domain properties; robust periodogram specification; Automata; Frequency-domain analysis; Limit-cycles; Mathematical model; Robustness; Voltage-controlled oscillators;
fLanguage
English
Publisher
ieee
Conference_Titel
Design and Diagnostics of Electronic Circuits & Systems, 17th International Symposium on
Conference_Location
Warsaw
Print_ISBN
978-1-4799-4560-3
Type
conf
DOI
10.1109/DDECS.2014.6868816
Filename
6868816
Link To Document