Title :
Formal verification of analog designs using MetiTarski
Author :
Denman, William ; Akbarpour, Behzad ; Tahar, Sofiene ; Zaki, Mohamed H. ; Paulson, Lawrence C.
Author_Institution :
Dept. of Electr. & Comput. Eng., Concordia Univ., Montreal, QC, Canada
Abstract :
MetiTarski, an automatic theorem prover for inequalities on real-valued elementary functions, can be used to verify properties of analog circuits. First, a closed form solution to the model of the circuit is obtained. We present two techniques for obtaining the closed form solution. One is based on piecewise linear modeling and the inverse Laplace transform. The other is based on small-signal analysis and transfer function theory. Second, the properties of interest are turned into a set of inequalities involving analytic functions, which are proved automatically using MetiTarski. We verify properties concerning oscillation and the change in gain due to component tolerances.
Keywords :
Laplace transforms; analogue integrated circuits; formal verification; piecewise linear techniques; theorem proving; transfer functions; MetiTarski; automatic theorem prover; closed form solution; formal verification analog design; inverse Laplace transform; piecewise linear modeling; real valued elementary functions; small signal analysis; solution model circuit; transfer function theory; Analog circuits; Analog computers; Closed-form solution; Computational modeling; Computer science; Formal verification; Inverse problems; Laboratories; Piecewise linear techniques; State-space methods;
Conference_Titel :
Formal Methods in Computer-Aided Design, 2009. FMCAD 2009
Conference_Location :
Austin, TX
Print_ISBN :
978-1-4244-4966-8
Electronic_ISBN :
978-1-4244-4966-8
DOI :
10.1109/FMCAD.2009.5351136
