Integrating Abstraction Techniques for Formal Verification of Analog Designs
Mohamed H. Zaki, William Denman, Sofiène Tahar, Guy Bois · Journal of Aerospace Computing Information and Communication · 2009
The verification of analog designs is a challenging and exhaustive task that requires deep understanding of physical behaviors. In this paper, we propose a qualitative-based predicate abstraction method for the verification of a class of nonlinear analog circuits. In the proposed method, system equations are automatically extracted from a circuit diagram by means of a bond graph. Verification is applied based on combining techniques from constraint solving and computer algebra along with symbolic model checking. Our methodology has the advantage of avoiding exhaustive simulation normally encountered in the verification of analog designs. To this end, we have used Dymola, Hsolver, SMV, and Mathematica to implement the verification flow. We illustrate the methodology on several analog examples including Colpitts and tunnel diode oscillators. I.