{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,21]],"date-time":"2024-05-21T12:10:05Z","timestamp":1716293405605},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,12,13]],"date-time":"2013-12-13T00:00:00Z","timestamp":1386892800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1007\/s10703-013-0204-6","type":"journal-article","created":{"date-parts":[[2013,12,12]],"date-time":"2013-12-12T10:52:48Z","timestamp":1386845568000},"page":"246-272","source":"Crossref","is-referenced-by-count":2,"title":["Verifying global start-up for a M\u00f6bius ring-oscillator"],"prefix":"10.1007","volume":"45","author":[{"given":"Chao","family":"Yan","sequence":"first","affiliation":[]},{"given":"Mark R.","family":"Greenstreet","sequence":"additional","affiliation":[]},{"given":"Suwen","family":"Yang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,12,13]]},"reference":[{"key":"204_CR1","first-page":"659","volume-title":"Proceedings of the 2011 international conference on computer aided design","author":"M Althoff","year":"2011","unstructured":"Althoff M, Rajhans A et al. (2011) Formal verification of phase-locked loops using reachability analysis and continuization. In: Proceedings of the 2011 international conference on computer aided design, pp\u00a0659\u2013666"},{"key":"204_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511804441","volume-title":"Convex optimization","author":"S Boyd","year":"2004","unstructured":"Boyd S, Vandenberghe L (2004) Convex optimization. Cambridge University Press, Cambridge"},{"key":"204_CR3","doi-asserted-by":"crossref","unstructured":"Cao Y (2008) PTM: predictive technology model. http:\/\/ptm.asu.edu","DOI":"10.1145\/1862891.1862892"},{"issue":"4","key":"204_CR4","doi-asserted-by":"crossref","first-page":"421","DOI":"10.1109\/T-C.1973.223730","volume":"C-22","author":"TJ Chaney","year":"1973","unstructured":"Chaney TJ, Molnar CE (1973) Anomalous behavior of synchronizer and arbiter circuits. IEEE Trans Comput C-22(4):421\u2013422","journal-title":"IEEE Trans Comput"},{"key":"204_CR5","first-page":"294","volume-title":"Proceedings of the 43 rd IEEE Midwest symposium on circuits and systems","author":"H Djahanshahi","year":"2000","unstructured":"Djahanshahi H, Salama CAT (2000) A two-stage differential CCO implementation in submicron CMOS. In: Proceedings of the 43 rd IEEE Midwest symposium on circuits and systems, pp\u00a0294\u2013297"},{"issue":"3","key":"204_CR6","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/s10703-006-0031-0","volume":"30","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle M (2007) HySAT: an efficient proof engine for bounded model checking of hybrid systems. Form Methods Syst Des 30(3):179\u2013198. doi: 10.1007\/s10703-006-0031-0","journal-title":"Form Methods Syst Des"},{"key":"204_CR7","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"Proceedings of the fifth international workshop on hybrid systems: computation and control","author":"G Frehse","year":"2005","unstructured":"Frehse G (2005) PHAVer: algorithmic verification of hybrid systems past HyTech. In: Proceedings of the fifth international workshop on hybrid systems: computation and control. LNCS, vol\u00a03414. Springer, Berlin, pp\u00a0258\u2013273"},{"key":"204_CR8","first-page":"257","volume-title":"Proceedings of design automation and test Europe","author":"G Frehse","year":"2006","unstructured":"Frehse G, Krogh BH, Rutenbar RA (2006) Verifying analog oscillator circuits using forward\/backward abstraction refinement. In: Proceedings of design automation and test Europe, pp\u00a0257\u2013262"},{"key":"204_CR9","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/1366110.1366160","volume-title":"Proceedings of the 18th great lakes symposium on VLSI (GLSVLSI\u201908)","author":"MR Greenstreet","year":"2008","unstructured":"Greenstreet MR, Yang S (2008) Verifying start-up conditions for a ring oscillator. In: Proceedings of the 18th great lakes symposium on VLSI (GLSVLSI\u201908), pp\u00a0201\u2013206"},{"key":"204_CR10","first-page":"210","volume-title":"Proceedings of 2004 IEEE\/ACM international conference on computer aided design","author":"S Gupta","year":"2004","unstructured":"Gupta S, Krogh BH, Rutenbar RA (2004) Towards formal verification of analog designs. In: Proceedings of 2004 IEEE\/ACM international conference on computer aided design, pp\u00a0210\u2013217"},{"key":"204_CR11","first-page":"542","volume-title":"Proceedings of the 39th ACM\/IEEE design automation conference","author":"W Hartong","year":"2002","unstructured":"Hartong W, Heidrich L, Barke E (2002) Model checking algorithms for analog verification. In: Proceedings of the 39th ACM\/IEEE design automation conference, pp\u00a0542\u2013547"},{"issue":"4","key":"204_CR12","doi-asserted-by":"crossref","first-page":"540","DOI":"10.1109\/9.664156","volume":"43","author":"TA Henzinger","year":"1998","unstructured":"Henzinger TA, Ho P-H, Wong-Toi H (1998) Algorithmic analysis of nonlinear hybrid systems. IEEE Trans Autom Control 43(4):540\u2013554","journal-title":"IEEE Trans Autom Control"},{"key":"204_CR13","first-page":"209","volume-title":"Proceedings international conference on computer design (ICCD)","author":"P Heydari","year":"2001","unstructured":"Heydari P, Pedram M (2001) Jitter-induced power\/ground noise in CMOS PLLs: a design perspective. In: Proceedings international conference on computer design (ICCD), pp\u00a0209\u2013213"},{"key":"204_CR14","volume-title":"Differential equations, dynamical systems, and linear algebra","author":"MW Hirsch","year":"1974","unstructured":"Hirsch MW, Smale S (1974) Differential equations, dynamical systems, and linear algebra. Academic Press, San Diego"},{"key":"204_CR15","volume-title":"Proc workshop on designing correct circuits","author":"KD Jones","year":"2008","unstructured":"Jones KD, Kim J, Konrad V (2008) Some \u201creal world\u201d problems in the analog and mixed-signal domains. In: Proc workshop on designing correct circuits"},{"key":"204_CR16","doi-asserted-by":"crossref","first-page":"613","DOI":"10.1109\/CICC.2009.5280741","volume-title":"Proceedings of the custom integrated circuits conference (CICC\u20192009)","author":"J Kim","year":"2009","unstructured":"Kim J, Jeeradit M, Lim B, Horowitz MA (2009) Leveraging designer\u2019s intent: a path toward simpler analog CAD tools. In: Proceedings of the custom integrated circuits conference (CICC\u20192009), pp\u00a0613\u2013620. doi: 10.1109\/CICC.2009.5280741"},{"key":"204_CR17","doi-asserted-by":"crossref","first-page":"1028","DOI":"10.1109\/TVLSI.2007.902207","volume":"15","author":"DJ Kinniment","year":"2007","unstructured":"Kinniment DJ, Dike C et al. (2007) Measuring deep metastability and its effect on synchronizer performance. IEEE Trans Very Large Scale Integr (VLSI) Syst 15:1028\u20131039","journal-title":"IEEE Trans Very Large Scale Integr (VLSI) Syst"},{"key":"204_CR18","unstructured":"Little S, Myers C (2008) Abstract modeling and simulation aided verification of analog\/mixed-signal circuits, Princeton, NJ, presented at the 2008 Workshop on Formal Verification for Analog Circuits (FAC\u201908)"},{"key":"204_CR19","first-page":"275","volume-title":"Proceedings of the international conference on computer aided design","author":"S Little","year":"2006","unstructured":"Little S, Seegmiller N, Walter D, Myers C, Yoneda T (2006) Verification of analog\/mixed-signal circuits using labeled hybrid Petri nets. In: Proceedings of the international conference on computer aided design, pp\u00a0275\u2013282"},{"key":"204_CR20","volume-title":"Proceedings of the third workshop on designing correct circuits","author":"I Mitchell","year":"1996","unstructured":"Mitchell I, Greenstreet M (1996) Proving Newtonian arbiters correct, almost surely. In: Proceedings of the third workshop on designing correct circuits, B\u00e5stad, Sweden"},{"key":"204_CR21","series-title":"Lecture notes in computer science","isbn-type":"print","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and algorithms for the construction and analysis of systems","author":"L Moura","year":"2008","unstructured":"Moura L, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Ramakrishnan CR, Rehof J (eds) Tools and algorithms for the construction and analysis of systems. Lecture notes in computer science, vol\u00a04963. Springer, Berlin, pp\u00a0337\u2013340. 978-3-540-78799-0","ISBN":"http:\/\/id.crossref.org\/isbn\/9783540787990"},{"key":"204_CR22","first-page":"469","volume-title":"Proceedings of the 29th European solid-state circuits conference (ESSCIRC\u201903)","author":"I Nissinen","year":"2003","unstructured":"Nissinen I, Mantyniemi A, Kostamovaara J (2003) A CMOS time-to-digital converter based on a ring oscillator for a laser radar. In: Proceedings of the 29th European solid-state circuits conference (ESSCIRC\u201903), pp\u00a0469\u2013472"},{"issue":"5","key":"204_CR23","doi-asserted-by":"crossref","first-page":"586","DOI":"10.1109\/4.760367","volume":"34","author":"C-H Park","year":"1999","unstructured":"Park C-H, Kim B (1999) A low-noise, 900MHz VCO in 0.6\u00a0\u03bc CMOS. IEEE J Solid-State Circuits 34(5):586\u2013591","journal-title":"IEEE J Solid-State Circuits"},{"key":"204_CR24","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511811555","volume-title":"A user\u2019s guide to measure theoretic probability","author":"D Pollard","year":"2001","unstructured":"Pollard D (2001) A user\u2019s guide to measure theoretic probability. Cambridge University Press, Cambridge"},{"key":"204_CR25","first-page":"77","volume-title":"Developments\u00a0in\u00a0reliable computing","author":"SM Rump","year":"1999","unstructured":"Rump SM (1999) INTLAB - INTerval LABoratory. In: Csendes T (ed) Developments\u00a0in\u00a0reliable computing. Kluwer Academic Publishers, Dordrecht, pp\u00a077\u2013104. http:\/\/www.ti3.tu-harburg.de\/rump\/"},{"issue":"1\u20132","key":"204_CR26","doi-asserted-by":"crossref","first-page":"567","DOI":"10.1016\/j.laa.2005.06.009","volume":"413","author":"SM Rump","year":"2006","unstructured":"Rump SM (2006) Eigenvalues, pseudospectrum and structured perturbations. Linear Algebra Appl 413(1\u20132):567\u2013593. doi: 10.1016\/j.laa.2005.06.009","journal-title":"Linear Algebra Appl"},{"key":"204_CR27","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1145\/2429384.2429423","volume-title":"2012 IEEE\/ACM international conference on computer-aided design (ICCAD)","author":"S Steinhorst","year":"2012","unstructured":"Steinhorst S, Hedrich L (2012) Trajectory-directed discrete state space modeling for formal verification of nonlinear analog circuits. In: 2012 IEEE\/ACM international conference on computer-aided design (ICCAD), pp\u00a0202\u2013209"},{"key":"204_CR28","doi-asserted-by":"crossref","first-page":"858","DOI":"10.1109\/ICSPS.2009.147","volume-title":"International conference on signal processing systems (ICSPS\u201909)","author":"S Steinhorst","year":"2009","unstructured":"Steinhorst S, Peter M, Hedrich L (2009) State space exploration of analog circuits by visualized multi-parallel particle simulation. In: International conference on signal processing systems (ICSPS\u201909), pp\u00a0858\u2013862"},{"key":"204_CR29","first-page":"5453","volume-title":"IEEE international symposium on circuits and systems (ISCAS)","author":"E Tatschl-Unterberger","year":"2005","unstructured":"Tatschl-Unterberger E, Cyrusian S, Ruegg M (2005) A\u00a02.5\u00a0GHz phase-switching PLL using a supply controlled 2-delay-stage 10\u00a0GHz ring oscillator for improved jitter\/mismatch. In: IEEE international symposium on circuits and systems (ISCAS), pp\u00a05453\u20135456"},{"key":"204_CR30","unstructured":"Tiwari SK, Gupta A et al (2008) fSpice: a Boolean satisfiability based approach for formally verifying analog circuits, Princeton, NJ, presented at the 2008 Workshop on Formal Verification for Analog Circuits (FAC\u201908)"},{"key":"204_CR31","volume-title":"Proceedings of the 2010 international conference on computer aided design","author":"SK Tiwari","year":"2010","unstructured":"Tiwari SK, Gupta A et al. (2010) First steps towards SAT-based formal analog verification. In: Proceedings of the 2010 international conference on computer aided design"},{"key":"204_CR32","first-page":"38","volume-title":"IEEE 32 nd annual power electronics specialists conference (PESC\u201901)","author":"J Xiao","year":"2001","unstructured":"Xiao J, Peterchev AV, Sanders SR (2001) Architecture and IC implementation of a digital VRM controller. In: IEEE 32 nd annual power electronics specialists conference (PESC\u201901), vol\u00a01, pp\u00a038\u201347"},{"key":"204_CR33","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1109\/ASPDAC.2008.4483985","volume-title":"Proceedings of the 2008 Asia and South Pacific design automation conference (ASPDAC\u201908)","author":"C Yan","year":"2008","unstructured":"Yan C, Greenstreet MR (2008) Faster projection based methods for circuit-level verification. In: Proceedings of the 2008 Asia and South Pacific design automation conference (ASPDAC\u201908), pp\u00a0410\u2013415"},{"key":"204_CR34","unstructured":"Zaki MH, Mitchell I, Greenstreet MR (2009) Towards a formal analysis of DC equilibria of analog designs, Grenoble, France. Presented at the 2009 Workshop on Formal Verification for Analog Circuits (FAC\u201909)"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0204-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-013-0204-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0204-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,21]],"date-time":"2024-05-21T11:46:12Z","timestamp":1716291972000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-013-0204-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12,13]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,10]]}},"alternative-id":["204"],"URL":"https:\/\/doi.org\/10.1007\/s10703-013-0204-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,12,13]]}}}