Abstract

Formal verification is one of the crucial stages of design phase that ensure the preciseness of the circuit design and its corresponding behavior with respect to specific system design. From last decade, there has been an abundant formal verification techniques introduced by the research community for analog and mixed signal circuits that used as an interface between analog and digital components. Owing to the maximized sophistication, and shrinking sizes of chip, analog, and mixed signal verification is encountering challenges in increasing verification requirement that calls for analyzing the prior techniques. The prime purpose of this paper is to discuss the most standard models, and techniques introduced till date and to excavate the various facts about their effectiveness in the area circuit design principles. The paper also discusses some of the critical research gaps explored from the study.

References

• Godse, A. P. , Bakshi, U. A. 2009. Electronic circuits. Technical Publications, pp. 744
• Veendrick, H. J. M. 2010. Nanometer CMOS ICs: From basics to ASICs. Springer Science & Business Media. Application-specific integrated circuits,pp. 762
• Brunvand, E. . 2010. Digital VLSI Chip Design with Cadence and Synopsys CAD Tools. Addison-Wesley, Computers, pp. 571
• Pratap, K. , Shelja, M. , Bedi, K. 2013. Formal Specification And Verification Of Reactive Systems. International Journal of Application or Innovation in Engineering & Management, Vol. 2, Iss. 3
• Darvas, D. , Adiego, B. F. , Voros, A. 2014. Formal veri_cation of complex properties on PLC programs. Springer
• Ziquan, T. , Shaojun, Y. , Yueming, J. , and Naiying, D. 2013. The Design of a Multi-bit Quantization Sigma-delta Modulator. International Journal of Signal Processing, Image Processing and Pattern Recognition, Vol. 6, No. 5, pp. 265-274
• Clarke, E. , Donze, A. . , Legay, A. . 2009. Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order ?? ? Modulator. Springer
• Cimatti, A. , Pecheur, C. , Cavada, R. 2003. Formal Verification of Diagnosability via Symbolic Model Checking. ACM-Proceedings of the 18th International Joint Conference on Artificial Intelligence, pp. 363-369
• Renesse, R. , Aghvami, A. H. 2004. Formal verification of Adhoc Routing protocols using SPIN Model Checker. IEEE MELECON
• Amla, N. , Du, X. . , Kuehlmann, A. , Kurshan, R. P. , and McMillan, K. L. 2005. An Analysis of SAT-based Model Checking Techniques in an Industrial Environment. Springer
• Mancini, T. , Mari, F. , Massini, A. . , Melatti, I. , Merli, F. , and Tronci, E. 2013. System Level Formal Verification via Model Checking Driven Simulation. Springer
• Barringer, H. , Goldberg, A. . , Havelund, K. . , and Sen, K. ,2004. Rule-Based Runtime Verification. Springer
• Meredith, P. N. , Jin, D. , Griffith, D. , Chen, F. , Rosu, G. 2012. An Overview of the MOP Runtime Verification Framework. Springer
• Chen, F. , Rosu, G. 2007. MOP: An Efficient and Generic Runtime Verification Framework. ACM press, pp 569-588
• Stoller, S. D. , Bartocci, E. . , Seyster, J. , Grosu, R. 2011. Runtime Verification with State Estimation. Proceedings of 2nd International Conference on Runtime verification, ACM-Springer, pp. 193-207
• Bartocci, E. . , Grosu, R. , Karmarkar, A. , Smolka, S. A. 2013. Adaptive Runtime Verification, Springer
• Harrison, M. D. , Masci, P. , Campos, J. C. , Curzon, P. 2013. Automated theorem proving for the systematic analysis of interactive Systems, Proceedings of the 5th International Workshop on Formal Methods for Interactive Systems
• Kapinski, J. , . Deshmukh, J. V. , Sankaranarayanan, S. , Aréchiga, N. 2014. Simulation-guided Lyapunov Analysis for Hybrid Dynamical Systems. ACM-Proceedings of the 17th international conference on Hybrid systems: computation and control, pp. 133-142
• Illan, D. A. , and Eder, K. 2014. Formal Veri_cation of Control Systems' Properties with Theorem Proving. arXiv:1405. 7615v2 [cs. SY]
• Abbasi, N. , Hasan, O. , Tahar, S. 2014. An approach for lifetime reliability analysis using theorem proving. Elsevier- Journal of Computer and System Sciences, Vol. 80, pp. 323–345
• Angelis, E. D. , Fioravanti, F. 2014. A Pettorossi, and M. Proietti, Verifying Array Programs by Transforming Verification Conditions, Springer
• Nakabayashi, T. . , Nakabayashi, K. , and Kako, F. 2014. An Equation-Based Circuit Design Technique for DC/DC Converters with Symbolic Computation System. International Journal Of Mathematics And Computers In Simulation, Vol. 8
• Tahar, S. , Akhras, I. , Nicolescu, G. 2013. On the Verification of a WiMax Design Using Symbolic Simulation. EPTCS, Vol. 122, pp. 23–37
• Wei, J. , Peng, Y. , Yu, G. , Greenstreet, M. 2013. Verifying Global Convergence for a Digital Phase-Locked Loop. IEEE-Formal Methods in Computer-Aided Design, pp. 113-120
• Yin, L. 2012. Formal Verification And In-Situ Test Of Analog And Mixed-Signal Circuits. Doctorial thesis of Texas A&M University
• Dang, T. , Donze, A. , Maler, O. 2004. Verification of Analog and Mixed-Signal Circuits using Hybrid System Techniques. Springer
• Tahar, S. , Zaki, M. H. , and Bois, G. 2006. Formal Verification of Analog and Mixed Signal Designs: Survey and Comparison. IEEE North-east Workshop on Circuits and Systems, pp. 281-284
• Tahar, S. , Sammane, G. A. , Zaki, M. H. 2007. A Symbolic Methodology for the Verification of Analog and Mixed Signal Designs. IEEE-Design, Automation & Test in Europe Conference, pp. 1-6
• Tahar, S. , Narayanan, R. , Akbarpour, B. 2010. Formal Verification of Analog Circuits in the Presence of Noise and Process Variation. IEEE-Design, Automation & Test in Europe Conference, pp. 1309-1312
• Ulus, D. , Sen, A. 2012. Using Haloes in Mixed-Signal Assertion Based Verification. IEEE-High Level Design validation and Test Workshop, pp. 49-55
• Goswami, D. , Chakraborty, S. , Bhaduri, P. , and Mitter, S. K. 2013. Characterizing Feedback Signal Drop Patterns in Formal Verification of Networked Control Systems. IEEE Conference on Computer Aided Control System Design, pp. 13-18
• Liang, C. 2013. Mixed-Signal Verification Methods for Multi-Power Mixed-Signal System-on-Chip (SoC) Design. IEEE10th International Conference on ASIC, pp. 1-4
• Balasubramanian, L. , Poluri, B. K. 2014. Efficient methods for analog mixed signal Verification. DVCON-Conference and Exhibition on Design and verification
• Materka, A. , and Strzelecki, M. 1996. Parametric Testing Of Mixed-Signal Circuits By ANN processing of transient responses. Journal of Electronic Testing, Vol. 9, Iss. 1-2, pp. 187-202
• Hartel, A. 2010. Improving and Testing a Mixed-Signal VLSI Neural Network Chip. Thesis of University of Heidelberg, Germany
• Manjunath, R. , Vasudev, S. , Udupa, N. 2010. Differential learning algorithm for Artificial Neural Networks. International Journal of Computer Applications, Vol. 1, No. 18