References:

[1]
Kundert, K., Chang, H., Jefferies, D., Lamant, G., Malavasi, E. and Sendig, F., Design of mixed-signal systems-on-a-chip. IEEE Trans. Computer-Aided Design Integrated Circuits Syst. v19 i12. 1561-1571.

[2]
Pecheux, F., Lallement, C. and Vachoux, A., VHDL-AMS and Verilog-AMS as alternative hardware description languages for efficient modeling of multidiscipline systems. IEEE Trans. Computer-Aided Design Integrated Circuits Syst. v24 i2. 204-225.

[3]
VHDL-AMS Language Reference Manual, 2004 {http://www.eda.org/vhdl-ams/}.

[4]
Verilog-AMS Language Reference Manual, 2004. Available from: {http://www.accellera.org}.

[5]
Rob A. Rutenbar , Brian A. Antao , Georges G. E. Gielen, Computer-Aided Design of Analog Integrated Circuits and Systems, John Wiley & Sons, Inc., New York, NY, 2002

[6]
Thomas Kropf, Introduction to Formal Hardware Verification: Methods and Tools for Designing Correct Circuits and Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1999

[7]
Rajeev Alur , Thomas A. Henzinger , Pei-Hsin Ho, Automatic Symbolic Verification of Embedded Systems, IEEE Transactions on Software Engineering, v.22 n.3, p.181-201, March 1996 [doi>10.1109/32.489079]

[8]
Clarke, E.M., Grumberg, O. and Peled, D.A., Model Checking. 2000. MIT Press, Cambridge, MA.

[9]
W. Hartong, R. Klausen, L. Hedrich, Formal Verification for Nonlinear Analog Systems: Approaches to Model and Equivalence Checking, Advanced Formal Verification, Kluwer, Dordrecht, 2004, pp. 205-245.

[10]
A. Balivada , Y. Hoskote , J. A. Abraham, Verification of transient response of linear analog circuits, Proceedings of the 13th IEEE VLSI Test Symposium (VTS'95), p.42, April 30-May 03, 1995

[11]
Suresh Seshadri , Jacob A. Abraham, Frequency Response Verification of Analog Circuits Using Global Optimization Techniques, Journal of Electronic Testing: Theory and Applications, v.17 n.5, p.395-408, October 2001 [doi>10.1023/A:1012751118746]

[12]
L. Hedrich , E. Barke, A formal approach to verification of linear analog circuits wth parameter tolerances, Proceedings of the conference on Design, automation and test in Europe, p.649-655, February 23-26, 1998, Le Palais des Congrés de Paris, France

[13]
Lars Hedrich , Erich Barke, A formal approach to nonlinear analog circuit verification, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.123-127, November 05-09, 1995, San Jose, California, United States

[14]
A. Salem, Semi-formal verification of VHDL-AMS descriptions, in: IEEE International Symposium on Circuits and Systems, 2002, pp. 333-336.

[15]
Henzinger, T.A., Ho, P.-H. and Wong-Toi, H., HyTech: a model checker for hybrid systems. Software Tools Technol. Transfer. v1 i1-2. 110-122.

[16]
Thomas A. Henzinger , Peter W. Kopke , Anuj Puri , Pravin Varaiya, What's decidable about hybrid automata?, Proceedings of the twenty-seventh annual ACM symposium on Theory of computing, p.373-382, May 29-June 01, 1995, Las Vegas, Nevada, United States [doi>10.1145/225058.225162]

[17]
Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994

[18]
Kurshan, R.P. and McMillan, K.L., Analysis of digital circuits through symbolic reduction. IEEE Trans. Computer-Aided Design. v10 i11. 1350-1371.

[19]
Mark R. Greenstreet, Verifying Safety Properties of Differential Equations, Proceedings of the 8th International Conference on Computer Aided Verification, p.277-287, August 03, 1996

[20]
Mark R. Greenstreet , Ian Mitchell, Integrating Projections, Proceedings of the First International Workshop on Hybrid Systems: Computation and Control, p.159-174, April 13-15, 1998

[21]
Chao Yan , Mark R. Greenstreet, Circuit Level Verification of a High-Speed Toggle, Proceedings of the Formal Methods in Computer Aided Design, p.199-206, November 11-14, 2007 [doi>10.1109/FMCAD.2007.16]

[22]
Mark R. Greenstreet , Ian Mitchell, Reachability Analysis Using Polygonal Projections, Proceedings of the Second International Workshop on Hybrid Systems: Computation and Control, p.103-116, March 29-31, 1999

[23]
T. Dang, A. Donze, O. Maler, Verification of analog and mixed-signal circuits using hybrid system techniques, in: Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science, vol. 3312, Springer, Berlin, 2004, pp. 14-17.

[24]
S. Gupta , B. H. Krogh , R. A. Rutenbar, Towards formal verification of analog designs, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.210-217, November 07-11, 2004 [doi>10.1109/ICCAD.2004.1382573]

[25]
Eugene Asarin , Thao Dang , Oded Maler, The d/dt Tool for Verification of Hybrid Systems, Proceedings of the 14th International Conference on Computer Aided Verification, p.365-370, July 27-31, 2002

[26]
Alberto Bemporad , Manfred Morari, Verification of Hybrid Systems via Mathematical Programming, Proceedings of the Second International Workshop on Hybrid Systems: Computation and Control, p.31-45, March 29-31, 1999

[27]
Chutinan, A. and Krogh, B.H., Computational techniques for hybrid system verification. IEEE Trans. Autom. Control. v48 i1. 64-75.

[28]
Goran Frehse , Bruce H. Krogh , Rob A. Rutenbar, Verifying analog oscillator circuits using forward/backward abstraction refinement, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany

[29]
G. Frehse, PHAVer: algorithmic verification of hybrid systems past HyTech, in: Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, vol. 3414, Springer, Berlin, 2005, pp. 258-273.

[30]
Mohamed H. Zaki , Ghiath Al-Sammane , Sofi`ene Tahar , Guy Bois, Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS Designs, Proceedings of the Formal Methods in Computer Aided Design, p.207-215, November 11-14, 2007 [doi>10.1109/FMCAD.2007.17]

[31]
Scott Little , Nicholas Seegmiller , David Walter , Chris Myers , Tomohiro Yoneda, Verification of analog/mixed-signal circuits using labeled hybrid petri nets, Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, November 05-09, 2006, San Jose, California [doi>10.1145/1233501.1233556]

[32]
Walter Hartong , Lars Hedrich , Erich Barke, Model checking algorithms for analog verification, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.514055]

[33]
Walter Hartong , Lars Hedrich , Erich Barke, On Discrete Modeling and Model Checking for Nonlinear Analog Systems, Proceedings of the 14th International Conference on Computer Aided Verification, p.401-413, July 27-31, 2002

[34]
S. Little, D. Walter, K. Jones, C.J. Myers, Analog/mixed-signal circuit verification using models generated from simulation traces, in: Automated Technology for Verification and Analysis, Lecture Notes in Computer Science, vol. 4762, Springer, Berlin, 2007, pp. 114-128.

[35]
Myers, C.J., Harrison, R.R., Walter, D., Seegmiller, N. and Little, S., The case for analog circuit verification. Electron. Notes Theor. Comput. Sci. v153 i3. 53-63.

[36]
Scott Little , Nicholas Seegmiller , David Walter , Chris Myers , Tomohiro Yoneda, Verification of analog/mixed-signal circuits using labeled hybrid petri nets, Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, November 05-09, 2006, San Jose, California [doi>10.1145/1233501.1233556]

[37]
L. Mendonça de Moura, B. Dutertre, N. Shankar, A tutorial on satisfiability modulo theories, in: Computer Aided Verification, Lecture Notes in Computer Science, vol. 4590, Springer, Berlin, 2007, pp. 20-36.

[38]
D. Walter , S. Little , N. Seegmiller , C. J. Myers , T. Yoneda, Symbolic Model Checking of Analog/Mixed-Signal Circuits, Proceedings of the 2007 conference on Asia South Pacific design automation, p.316-323, January 23-26, 2007 [doi>10.1109/ASPDAC.2007.358005]

[39]
D. Walter, S. Little, C. Myers, Bounded model checking of analog and mixed-signal circuits using an SMT solver, in: Automated Technology for Verification and Analysis, Lecture Notes in Computer Science, vol. 4762, Springer, Berlin, 2007, pp. 66-81.

[40]
Grabowski, D., Platte, D., Hedrich, L. and Barke, E., Time constrained verification of analog circuits using model-checking algorithms. Electron. Notes Theor. Comput. Sci. v153 i3. 37-52.

[41]
S. Steinhorst, A. Jesser, L. Hedrich, Advanced property specification for model checking of analog systems, in: Analog'06, 2006, pp. 63-68.

[42]
Freibothe, M., Schönherr, J. and Straube, B., Formal verification of the quasi-static behavior of mixed-signal circuits by property checking. Electron. Notes Theor. Comput. Sci. v153 i3. 23-35.

[43]
Jun Yuan , Carl Pixley , Adnan Aziz, Constraint-Based Verification, Springer-Verlag New York, Inc., Secaucus, NJ, 2006

[44]
Tan, L., Kim, J. and Lee, I., Testing and monitoring model-based generated program. Electron. Notes Theor. Comput. Sci. v89 i2. 128-148.

[45]
O. Maler, D. Nickovic, A. Pnueli, Real-time temporal logic: past, present, future, in: Formal Modelling and Analysis of Timed Systems, Lecture Notes in Computer Science, vol. 3829, Springer, Berlin, 2005, pp. 2-16.

[46]
O. Maler, D. Nickovic, Monitoring temporal properties of continuous signals, in: Formal Modelling and Analysis of Timed Systems, Lecture Notes in Computer Science, vol. 3253, Springer, Berlin, 2004, pp. 152-166.

[47]
Accellera Property Specification Language Reference Manual, 2004. Available from: {http://www.accellera.org}.

[48]
Thati, P. and Rosu, G., Monitoring algorithms for metric temporal logic specifications. Electron. Notes Theor. Comput. Sci. v113. 145-162.

[49]
O. Maler, D. Nickovic, A. Pnueli, From MITL to timed automata, in: Formal Modelling and Analysis of Timed Systems, Lecture Notes in Computer Science, vol. 4202, Springer, Berlin, 2006, pp. 274-289.

[50]
D. Nickovic, O. Maler, AMT: a property-based monitoring tool for analog systems, in: Formal Modelling and Analysis of Timed Systems, Austria, Lecture Notes in Computer Science, vol. 4763, Springer, Berlin, 2007, pp. 304-319.

[51]
G. Al Sammane, M. Zaki, Z.J. Dong, S. Tahar, Towards assertion based verification of analog and mixed signal designs using PSL, in: Languages for Formal Specification and Verification, Forum on Specification and Design Languages, 2007.

[52]
Tathagato Rai Dastidar , P. P. Chakrabarti, A Verification System for Transient Response of Analog Circuits Using Model Checking, Proceedings of the 18th International Conference on VLSI Design held jointly with 4th International Conference on Embedded Systems Design, p.195-200, January 03-07, 2005 [doi>10.1109/ICVD.2005.38]

[53]
Tathagato Rai Dastidar , P. P. Chakrabarti, A verification system for transient response of analog circuits, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.12 n.3, p.1-39, August 2007 [doi>10.1145/1255456.1255468]

[54]
Frehse, G., Krogh, B., Rutenbar, R. and Maler, O., Time domain verification of oscillator circuit properties. Electron. Notes Theor. Comput. Sci. v153 i3. 9-22.

[55]
Mohamed H. Zaki , Sofiène Tahar , Guy Bois, A practical approach for monitoring analog circuits, Proceedings of the 16th ACM Great Lakes symposium on VLSI, April 30-May 01, 2006, Philadelphia, PA, USA [doi>10.1145/1127908.1127984]

[56]
Formal Verification of Synthesized Analog Designs, Proceedings of the 1999 IEEE International Conference on Computer Design, p.40, October 10-13, 1999

[57]
Keith Hanna, Reasoning About Analog-Level Implementationsof Digital Systems, Formal Methods in System Design, v.16 n.2, p.127-158, March 2000 [doi>10.1023/A:1008791128550]

[58]
Keith Hanna, Reasoning about Real Circuits, Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and Its Applications, p.235-253, September 19-22, 1994

[59]
F. Keith Hanna, Automatic Verification of Mixed-Level Logic Circuits, Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, p.133-166, November 04-06, 1998

[60]
Ghiath Al-Sammane , Mohamed H. Zaki , Sofiène Tahar, A symbolic methodology for the verification of analog and mixed signal designs, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France