{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:52:31Z","timestamp":1759146751412,"version":"3.41.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2007,8,17]],"date-time":"2007-08-17T00:00:00Z","timestamp":1187308800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2007,8,17]]},"abstract":"<jats:p>We present a method for application of formal techniques like model checking and equivalence checking for validation of the transient response of nonlinear analog circuits. We propose a temporal logic called Ana CTL (computational tree logic for analog circuit verification) which is suitable for specifying properties specific to analog circuits. The application of Ana CTL for validation of transient behavior of arbitrarily nonlinear analog circuits is presented. The transient response of a circuit under all possible input waveforms is represented as a finite state machine (FSM), by bounding and discretizing the continuous state space of an analog circuit. We have developed algorithms to run Ana CTL queries on this discretized model using search-based methods which reduce the runtime considerably by avoiding creation of the whole FSM. The application of these methods on several real-life analog circuits is presented and we show that this system is a useful aid for detecting and debugging early design errors.<\/jats:p>\n          <jats:p>\n            We also present methods for checking the equivalence of transient response of two analog circuits. The behavior of two different analog circuits can rarely be exactly similar. Hence, we introduce a notion of\n            <jats:italic>approximate<\/jats:italic>\n            equivalence. A query language for checking different notions of user-definable approximate equivalence is presented which extends the syntax of the Ana CTL model checking language. In its extended form, Ana CTL can be used combining model checking with equivalence checking.\n          <\/jats:p>","DOI":"10.1145\/1255456.1255468","type":"journal-article","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T13:44:55Z","timestamp":1189777495000},"page":"1-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["A verification system for transient response of analog circuits"],"prefix":"10.1145","volume":"12","author":[{"given":"Tathagato Rai","family":"Dastidar","sequence":"first","affiliation":[{"name":"Xaneda Technologies, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P. P.","family":"Chakrabarti","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology, Kharagpur, India"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,5,22]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Accellera. 2004. Verilog AMS. http:\/\/www.eda.org\/verilog-ams\/.  Accellera. 2004. Verilog AMS. http:\/\/www.eda.org\/verilog-ams\/."},{"key":"e_1_2_1_2_1","unstructured":"Allen P. E. and Holberg D. R. 1987. CMOS Analog Circuit Design. Oxford University Press.  Allen P. E. and Holberg D. R. 1987. CMOS Analog Circuit Design. Oxford University Press."},{"volume-title":"Proceedings of the 10th International Conference on Concurrency Theory (CONCUR). 98--113","author":"Alur R.","key":"e_1_2_1_3_1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.489079"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_6_1","unstructured":"Analog Insydes. 2007. Analog Insydes version 2.1. http:\/\/www.analog-inydes.de\/.  Analog Insydes. 2007. Analog Insydes version 2.1. http:\/\/www.analog-inydes.de\/."},{"volume-title":"Proceedings of the 13th IEEE VLSI Test Symposium (VTC). 42--47","author":"Balivada A.","key":"e_1_2_1_7_1"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1080334.1080337"},{"volume-title":"Proceedings of the 40th IEEE Conference on Decision and Control. 2881--2886","author":"Behrmann G.","key":"e_1_2_1_9_1"},{"volume-title":"Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 193--207","author":"Biere A.","key":"e_1_2_1_10_1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.275352"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2002.806655"},{"key":"e_1_2_1_13_1","unstructured":"Clarke E. M. Jr. Grumberg O. and Peled D. A. 2000. Model Checking. MIT Press Cambridge MA.  Clarke E. M. Jr. Grumberg O. and Peled D. A. 2000. Model Checking. MIT Press Cambridge MA."},{"key":"e_1_2_1_14_1","unstructured":"Cormen T. H. Leiserson C. E. and Rivest R. E. 1990. Introduction to Algorithms. MIT Press Cambridge MA.   Cormen T. H. Leiserson C. E. and Rivest R. E. 1990. Introduction to Algorithms. MIT Press Cambridge MA."},{"key":"e_1_2_1_15_1","unstructured":"Dang T. and Maler O. 2000. d\/dt: Reachability analysis of continuous and hybrid systems. http:\/\/www-verimag.imag.fr\/~tdang\/ddt.html.  Dang T. and Maler O. 2000. d\/dt: Reachability analysis of continuous and hybrid systems. http:\/\/www-verimag.imag.fr\/~tdang\/ddt.html."},{"volume-title":"Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD) (Nov.).","author":"Dang T.","key":"e_1_2_1_16_1"},{"volume-title":"Proceedings of the Asia and South Pacific Design Automation Conference (ASP-DAC). 735--740","author":"Dasgupta P.","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICVD.2005.38"},{"volume-title":"Proceedings of the Conference and Exhibtion on Design, Automation and Test in Europe (DATE). 257--262","author":"Frehse G.","key":"e_1_2_1_19_1"},{"volume-title":"Proceedings of the ACM\/IEEE International Conference on Computer Design. 40--45","author":"Ghosh A.","key":"e_1_2_1_20_1"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382573"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/513918.514055"},{"volume-title":"Proceedings of the 14th International Conference on Computer-Aided Verification. 401--413","author":"Hartong W.","key":"e_1_2_1_23_1"},{"volume-title":"Symbolic Approximation and Modeling Techniques for Analysis and Design of Analog Circuits","author":"Hennig E.","key":"e_1_2_1_24_1"},{"volume-title":"Fundamentals of Computer-Aided Circuits Simulation","author":"McCalla W. J.","key":"e_1_2_1_25_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-2011-1"},{"key":"e_1_2_1_26_1","unstructured":"NuSMV. 2007. NuSMV: A new symbolic model checker. http:\/\/nusmv.irst.itc.it\/.  NuSMV. 2007. NuSMV: A new symbolic model checker. http:\/\/nusmv.irst.itc.it\/."},{"key":"e_1_2_1_27_1","unstructured":"PHAVer. 2006. PHAVer: Polyhedral hybrid automaton verifyer. http:\/\/www.cs.ru.nl\/~goranf\/.  PHAVer. 2006. PHAVer: Polyhedral hybrid automaton verifyer. http:\/\/www.cs.ru.nl\/~goranf\/."},{"key":"e_1_2_1_28_1","unstructured":"Quarles T. Pederson D. Newton R. Sangiovanni-Vincentelli A. and Wayne C. 2007. The Spice page. http:\/\/bwrc.eecs.berkeley.edu\/Classes\/IcBook\/SPICE.  Quarles T. Pederson D. Newton R. Sangiovanni-Vincentelli A. and Wayne C. 2007. The Spice page. http:\/\/bwrc.eecs.berkeley.edu\/Classes\/IcBook\/SPICE."},{"volume-title":"The Spice3 implementation guide. Memorandum no. UCB\/ERL M89\/44","author":"Quarles T. L.","key":"e_1_2_1_29_1"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205179"},{"volume-title":"Proceedings of the 40th IEEE Conference on Decision and Control. 2867--2874","author":"Silva B. I.","key":"e_1_2_1_31_1"},{"key":"e_1_2_1_32_1","first-page":"7","article-title":"Compact representation and efficient generation of s-expanded symbolic network functions for computer-aided analog circuit design","volume":"20","author":"Tan S. X.-D.","year":"2001","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circ. Syst."}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1255456.1255468","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1255456.1255468","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:22:28Z","timestamp":1750278148000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1255456.1255468"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,8,17]]},"references-count":32,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,8,17]]}},"alternative-id":["10.1145\/1255456.1255468"],"URL":"https:\/\/doi.org\/10.1145\/1255456.1255468","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2007,8,17]]},"assertion":[{"value":"2005-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-05-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}