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
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;
Conference_Titel :
Design and Diagnostics of Electronic Circuits & Systems, 17th International Symposium on
Conference_Location :
Warsaw
Print_ISBN :
978-1-4799-4560-3
DOI :
10.1109/DDECS.2014.6868816
