Zaki, Mohamed H., Tahar, Sofiène and Bois, Guy (2008) Formal verification of analog and mixed signal designs: A survey. Microelectronics Journal, 39 (12). pp. 13951404. ISSN 00262692

Text (application/pdf)
212kBMEJ2008.pdf  Accepted Version 
Official URL: http://dx.doi.org/10.1016/j.mejo.2008.05.013
Abstract
Analog and mixed signal (AMS) designs are an important part of embedded systems that link digital designs to the analog world. Due to challenges associated with its verification process, AMS designs require a considerable portion of the total design cycle time. In contrast to digital designs, the verification of AMS systems is a challenging task that requires lots of expertise and deep understanding of their behavior. Researchers started lately studying the applicability of formal methods for the verification of AMS systems as a way to tackle the limitations of conventional verification methods like simulation. This paper surveys research activities in the formal verification of AMS designs as well as compares the different proposed approaches.
Divisions:  Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering 

Item Type:  Article 
Refereed:  Yes 
Authors:  Zaki, Mohamed H. and Tahar, Sofiène and Bois, Guy 
Journal or Publication:  Microelectronics Journal 
Date:  2008 
Digital Object Identifier (DOI):  10.1016/j.mejo.2008.05.013 
Keywords:  analog and mixed signal design verification; design electronics; formal verification; performance; realtime and embedded systems reliability, testing, and faulttolerance; signal processing systems; survey; theory; verification 
ID Code:  977369 
Deposited By:  DANIELLE DENNIE 
Deposited On:  14 Jun 2013 14:28 
Last Modified:  18 Jan 2018 17:44 
References:
[1]Kundert, K., Chang, H., Jefferies, D., Lamant, G., Malavasi, E. and Sendig, F., Design of mixedsignal systemsonachip. IEEE Trans. ComputerAided Design Integrated Circuits Syst. v19 i12. 15611571.
[2]
Pecheux, F., Lallement, C. and Vachoux, A., VHDLAMS and VerilogAMS as alternative hardware description languages for efficient modeling of multidiscipline systems. IEEE Trans. ComputerAided Design Integrated Circuits Syst. v24 i2. 204225.
[3]
VHDLAMS Language Reference Manual, 2004 {http://www.eda.org/vhdlams/}.
[4]
VerilogAMS Language Reference Manual, 2004. Available from: {http://www.accellera.org}.
[5]
Rob A. Rutenbar , Brian A. Antao , Georges G. E. Gielen, ComputerAided 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, SpringerVerlag New York, Inc., Secaucus, NJ, 1999
[7]
Rajeev Alur , Thomas A. Henzinger , PeiHsin Ho, Automatic Symbolic Verification of Embedded Systems, IEEE Transactions on Software Engineering, v.22 n.3, p.181201, 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. 205245.
[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 30May 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.395408, 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.649655, February 2326, 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 Computeraided design, p.123127, November 0509, 1995, San Jose, California, United States
[14]
A. Salem, Semiformal verification of VHDLAMS descriptions, in: IEEE International Symposium on Circuits and Systems, 2002, pp. 333336.
[15]
Henzinger, T.A., Ho, P.H. and WongToi, H., HyTech: a model checker for hybrid systems. Software Tools Technol. Transfer. v1 i12. 110122.
[16]
Thomas A. Henzinger , Peter W. Kopke , Anuj Puri , Pravin Varaiya, What's decidable about hybrid automata?, Proceedings of the twentyseventh annual ACM symposium on Theory of computing, p.373382, May 29June 01, 1995, Las Vegas, Nevada, United States [doi>10.1145/225058.225162]
[17]
Robert P. Kurshan, Computeraided verification of coordinating processes: the automatatheoretic approach, Princeton University Press, Princeton, NJ, 1994
[18]
Kurshan, R.P. and McMillan, K.L., Analysis of digital circuits through symbolic reduction. IEEE Trans. ComputerAided Design. v10 i11. 13501371.
[19]
Mark R. Greenstreet, Verifying Safety Properties of Differential Equations, Proceedings of the 8th International Conference on Computer Aided Verification, p.277287, August 03, 1996
[20]
Mark R. Greenstreet , Ian Mitchell, Integrating Projections, Proceedings of the First International Workshop on Hybrid Systems: Computation and Control, p.159174, April 1315, 1998
[21]
Chao Yan , Mark R. Greenstreet, Circuit Level Verification of a HighSpeed Toggle, Proceedings of the Formal Methods in Computer Aided Design, p.199206, November 1114, 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.103116, March 2931, 1999
[23]
T. Dang, A. Donze, O. Maler, Verification of analog and mixedsignal circuits using hybrid system techniques, in: Formal Methods in ComputerAided Design, Lecture Notes in Computer Science, vol. 3312, Springer, Berlin, 2004, pp. 1417.
[24]
S. Gupta , B. H. Krogh , R. A. Rutenbar, Towards formal verification of analog designs, Proceedings of the 2004 IEEE/ACM International conference on Computeraided design, p.210217, November 0711, 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.365370, July 2731, 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.3145, March 2931, 1999
[27]
Chutinan, A. and Krogh, B.H., Computational techniques for hybrid system verification. IEEE Trans. Autom. Control. v48 i1. 6475.
[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 0610, 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. 258273.
[30]
Mohamed H. Zaki , Ghiath AlSammane , 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.207215, November 1114, 2007 [doi>10.1109/FMCAD.2007.17]
[31]
Scott Little , Nicholas Seegmiller , David Walter , Chris Myers , Tomohiro Yoneda, Verification of analog/mixedsignal circuits using labeled hybrid petri nets, Proceedings of the 2006 IEEE/ACM international conference on Computeraided design, November 0509, 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 1014, 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.401413, July 2731, 2002
[34]
S. Little, D. Walter, K. Jones, C.J. Myers, Analog/mixedsignal 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. 114128.
[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. 5363.
[36]
Scott Little , Nicholas Seegmiller , David Walter , Chris Myers , Tomohiro Yoneda, Verification of analog/mixedsignal circuits using labeled hybrid petri nets, Proceedings of the 2006 IEEE/ACM international conference on Computeraided design, November 0509, 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. 2036.
[38]
D. Walter , S. Little , N. Seegmiller , C. J. Myers , T. Yoneda, Symbolic Model Checking of Analog/MixedSignal Circuits, Proceedings of the 2007 conference on Asia South Pacific design automation, p.316323, January 2326, 2007 [doi>10.1109/ASPDAC.2007.358005]
[39]
D. Walter, S. Little, C. Myers, Bounded model checking of analog and mixedsignal circuits using an SMT solver, in: Automated Technology for Verification and Analysis, Lecture Notes in Computer Science, vol. 4762, Springer, Berlin, 2007, pp. 6681.
[40]
Grabowski, D., Platte, D., Hedrich, L. and Barke, E., Time constrained verification of analog circuits using modelchecking algorithms. Electron. Notes Theor. Comput. Sci. v153 i3. 3752.
[41]
S. Steinhorst, A. Jesser, L. Hedrich, Advanced property specification for model checking of analog systems, in: Analog'06, 2006, pp. 6368.
[42]
Freibothe, M., Schönherr, J. and Straube, B., Formal verification of the quasistatic behavior of mixedsignal circuits by property checking. Electron. Notes Theor. Comput. Sci. v153 i3. 2335.
[43]
Jun Yuan , Carl Pixley , Adnan Aziz, ConstraintBased Verification, SpringerVerlag New York, Inc., Secaucus, NJ, 2006
[44]
Tan, L., Kim, J. and Lee, I., Testing and monitoring modelbased generated program. Electron. Notes Theor. Comput. Sci. v89 i2. 128148.
[45]
O. Maler, D. Nickovic, A. Pnueli, Realtime temporal logic: past, present, future, in: Formal Modelling and Analysis of Timed Systems, Lecture Notes in Computer Science, vol. 3829, Springer, Berlin, 2005, pp. 216.
[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. 152166.
[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. 145162.
[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. 274289.
[50]
D. Nickovic, O. Maler, AMT: a propertybased 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. 304319.
[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.195200, January 0307, 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.139, 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. 922.
[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 30May 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 1013, 1999
[57]
Keith Hanna, Reasoning About AnalogLevel Implementationsof Digital Systems, Formal Methods in System Design, v.16 n.2, p.127158, 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.235253, September 1922, 1994
[59]
F. Keith Hanna, Automatic Verification of MixedLevel Logic Circuits, Proceedings of the Second International Conference on Formal Methods in ComputerAided Design, p.133166, November 0406, 1998
[60]
Ghiath AlSammane , 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 1620, 2007, Nice, France
Repository Staff Only: item control page