{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:17:54Z","timestamp":1755217074705,"version":"3.43.0"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2000,10,1]],"date-time":"2000-10-01T00:00:00Z","timestamp":970358400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,10,1]],"date-time":"2000-10-01T00:00:00Z","timestamp":970358400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2000,10]]},"DOI":"10.1023\/a:1008748802907","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T11:37:32Z","timestamp":1040557052000},"page":"107-134","source":"Crossref","is-referenced-by-count":1,"title":["Verification of Similar FSMs by Mixing Incremental Re-encoding, Reachability Analysis, and Combinational Checks"],"prefix":"10.1007","volume":"17","author":[{"given":"Stefano","family":"Quer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gianpiero","family":"Cabodi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paolo","family":"Camurati","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luciano","family":"Lavagno","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ellen M.","family":"Sentovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert K.","family":"Brayton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"268970_CR1","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1109\/54.262320","volume":"11","author":"E.J. Aas","year":"1994","unstructured":"E.J. Aas, T. Steen, and K. Klingsheim, \u201cQuantifying design quality though design experiments,\u201d IEEE Design and Test, Vol. 11, pp. 27\u201337, 1994.","journal-title":"IEEE Design and Test"},{"issue":"1","key":"268970_CR2","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1109\/43.3141","volume":"7","author":"M.S. Abadir","year":"1988","unstructured":"M.S. Abadir, J. Ferguson, and T.E. Kirkland, \u201cLogin design verification via test generation,\u201d IEEE Transactions on CAD, Vol. 7, No. 1, pp. 138\u2013148, Jan. 1988.","journal-title":"IEEE Transactions on CAD"},{"doi-asserted-by":"crossref","unstructured":"P. Ashar, A. Gupta, and S. Malik, \u201cUsing complete-1-distinguishability for FSM equivalence checking,\u201d in Proc. IEEE\/ACM ICCAD'96, San Jose, California, Nov. 1996, pp. 346\u2013353.","key":"268970_CR3","DOI":"10.1109\/ICCAD.1996.569807"},{"issue":"4","key":"268970_CR4","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J.R. Burch","year":"1994","unstructured":"J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, and D.L. Dill, \u201cSymbolic model checking for sequential circuit verification,\u201d IEEE Transactions on CAD, Vol. 13, No. 4, pp. 401\u2013424, 1994.","journal-title":"IEEE Transactions on CAD"},{"key":"268970_CR5","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1023\/A:1008632417306","volume":"12","author":"G. Cabodi","year":"1998","unstructured":"G. Cabodi, P. Camurati, F. Corno, P. Prinetto, and M.S. Reorda, \u201cThe general product machine: A new model for symbolic FSM traversal,\u201d Formal Methods in Systems Design, Vol. 12, pp. 267\u2013289, 1998.","journal-title":"Formal Methods in Systems Design"},{"doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, and S. Quer, \u201cEfficient state space pruning in symbolic backward traversal,\u201d in Proc. IEEE ICCD'94, Cambridge, Massachussetts, Oct. 1994, pp. 230\u2013235.","key":"268970_CR6","DOI":"10.1109\/ICCD.1994.331895"},{"doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, and S. Quer, \u201cImproved reachability analysis of large finite state machine,\u201d in Proc. IEEE\/ACM ICCAD'96, San Jose, California, Nov. 1996, pp. 354\u2013360.","key":"268970_CR7","DOI":"10.1109\/ICCAD.1996.569819"},{"unstructured":"B. Chen, C.L. Lee, and J.E. Chen, \u201cDesign verification by using universal test sets,\u201d in Proc. Asian Test Symposium, 1994, pp. 261\u2013266.","key":"268970_CR8"},{"doi-asserted-by":"crossref","unstructured":"D.I. Cheng and M. Marek-Sadowska, \u201cVerifying equivalence of functions with unknown input correspondence,\u201d in Proc. EDAC'93, Feb. 1993, pp. 81\u201385.","key":"268970_CR9","DOI":"10.1109\/EDAC.1993.386496"},{"doi-asserted-by":"crossref","unstructured":"H. Cho, G. Hachtel, S.W. Jeong, B. Plessier, E. Schwarz, and F. Somenzi, \u201cATPG aspects of FSM verification,\u201d in Proc. IEEE ICCAD'90, San Jose, California, Nov. 1990, pp. 134\u2013137.","key":"268970_CR10","DOI":"10.1109\/ICCAD.1990.129861"},{"unstructured":"H. Cho, G. Hachtel, E. Macii, M. Poncino, and F. Somenzi, \u201cA structural approach to state space decomposition for approximate reachability analysis,\u201d in Proc. IEEE ICCD'94, Cambridge, Massechussets, Oct. 1994, pp. 236\u2013239.","key":"268970_CR11"},{"doi-asserted-by":"crossref","unstructured":"H. Cho, G.D. Hatchel, E. Macii, B. Plessier, and F. Somenzi, \u201cAlgorithms for approximate FSM traversal,\u201d in Proc. ACM\/IEEE DAC'93, Dallas, Texas, June 1993, pp. 25\u201330.","key":"268970_CR12","DOI":"10.1145\/157485.164555"},{"unstructured":"H. Cho, G.D. Hatchel, E. Macii, M. Poncino, K. Ravi, and F. Somenzi, \u201cApproximate finite state machine traversal: Extensions and new results,\u201d in IWLS'95: IEEE International Workshop on Logic Synthesis, Lake Tahoe, California, May 1995.","key":"268970_CR13"},{"key":"268970_CR14","first-page":"365","volume-title":"Lecture Notes in Computer Science","author":"O. Coudert","year":"1989","unstructured":"O. Coudert, C. Berthet, and J.C. Madre, \u201cVerification of sequential machines based on symbolic execution,\u201d Lecture Notes in Computer Science 407, Springer Verlag, Berlin, Germany, 1989, pp. 365\u2013373."},{"key":"268970_CR15","first-page":"111","volume":"1","author":"O. Coudert","year":"1989","unstructured":"O. Coudert, C. Berthet, and J.C. Madre, \u201cVerification of sequential machines using Boolean function vectors,\u201d in Proc. IFIP Int'l Workshop on Applied Formal Methods for Correct VLSI Design, Vol. 1, Nov. 1989, pp. 111\u2013128.","journal-title":"Proc. IFIP Int'l Workshop on Applied Formal Methods for Correct VLSI Design"},{"doi-asserted-by":"crossref","unstructured":"T. Filkorn, \u201cA method for symbolic verification of synchronous circuits,\u201d in Proc. IFIP CHDL'91, April 1991, pp. 229\u2013239.","key":"268970_CR16","DOI":"10.1016\/B978-0-444-89208-9.50020-X"},{"doi-asserted-by":"crossref","unstructured":"U. Glaser and K.-T. Cheng, \u201cLogic optimization by an improved sequential redundancy addition and removal technique,\u201d in Proc. ASP-DAC'95, Aug. 1995, pp. 235\u2013240.","key":"268970_CR17","DOI":"10.1109\/ASPDAC.1995.486229"},{"doi-asserted-by":"crossref","unstructured":"G. Hachtel and F. Somenzi, \u201cA symbolic algorithm for maximum flow in 0-1 networks,\u201d in Proc. IEEE ICCAD'93, San Jose, California, Nov. 1993, pp. 403\u2013406.","key":"268970_CR18","DOI":"10.1109\/ICCAD.1993.580088"},{"unstructured":"G. Hachtel and F. Somenzi, Logic Synthesis and Verification Algorithms. Kluwer Academic Publishers, 1996.","key":"268970_CR19"},{"doi-asserted-by":"crossref","unstructured":"S. Krischer, \u201cThe backward walk approach in FSM verification,\u201d in Proc. IFIP CHDL'93, April 1993, pp. 143\u2013150.","key":"268970_CR20","DOI":"10.1016\/B978-0-444-81641-2.50018-6"},{"issue":"1","key":"268970_CR21","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1147\/rd.391.0149","volume":"39s.","author":"A. Kuehlmann","year":"1995","unstructured":"A. Kuehlmann, A. Srinivasan, and D.P. LaPotin, \u201cVerity\u2013A formal verification program for custom CMOS circuits,\u201d IBM Journal of Research and Development, Vol. 39, Nos. 1\/2, pp. 149\u2013165, Jan.-March 1995.","journal-title":"IBM Journal of Research and Development"},{"doi-asserted-by":"crossref","unstructured":"A. Kuehlmann and F. Krohm, \u201cEquivalence checking using cuts and heaps,\u201d in Proc. EDA\/SIGDA\/ACM\/IEEE DAC'97, Anaheim, California, June 1997, pp. 263\u2013268.","key":"268970_CR22","DOI":"10.1145\/266021.266090"},{"doi-asserted-by":"crossref","unstructured":"B. Lin and A. Richard Newton, \u201cImplicit manipulation of equivalence classes using binary decision diagrams,\u201d in Proc. IEEE ICCD'91, Oct. 1991, pp. 81\u201385.","key":"268970_CR23","DOI":"10.1109\/ICCD.1991.139995"},{"doi-asserted-by":"crossref","unstructured":"B. Lin, H.J. Touati, and A. Richard Newton, \u201cDon't care minimization of multi-level sequential logic networks,\u201d in Proc. IEEE ICCAD'90, San Jose, California, Nov. 1990, pp. 414\u2013417.","key":"268970_CR24","DOI":"10.1109\/ICCAD.1990.129940"},{"key":"268970_CR25","volume-title":"Synthesis and Optimization of Digital Circuits","author":"G. De Micheli","year":"1994","unstructured":"G. De Micheli, Synthesis and Optimization of Digital Circuits. McGraw Hill, Hightstown, New Jersey, 1994."},{"doi-asserted-by":"crossref","unstructured":"A. Narayan, J. Jain, M. Fujita, and A. Sangiovanni-Vincentelli, \u201cPartitioned ROBDDs\u2013A compact, canonical and efficient manipulable representation of Boolean functions,\u201d in Proc. IEEE\/ACM ICCAD'96, San Jose, California, Nov. 1996, pp. 547\u2013554.","key":"268970_CR26","DOI":"10.1109\/ICCAD.1996.569909"},{"key":"268970_CR27","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1090\/dimacs\/003\/20","volume":"3","author":"C. Pixley","year":"1991","unstructured":"C. Pixley, \u201cA computational theory and implementation of sequential hardware equivalence,\u201d AMS\/DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, pp. 293\u2013320, 1991.","journal-title":"AMS\/DIMACS Series in Discrete Mathematics and Theoretical Computer Science"},{"unstructured":"S. Quer, G. Cabodi, P. Camurati, L. Lavagno, E.M. Sentovich, and R.K. Brayton, \u201cLarge incremental FSM re-encoding for simplifying verification by symbolic traversal,\u201d in IWLS'95: IEEE International Workshop on Logic Synthesis, May 1995, pp. 3.17\u20133.27.","key":"268970_CR28"},{"doi-asserted-by":"crossref","unstructured":"S. Quer, G. Cabodi, P. Camurati, L. Lavagno, E.M. Sentovich, and R.K. Brayton, \u201cIncremental re-encoding for symbolic traversal of product machines,\u201d in Proc. IEEE EURO-DAC'96, Geneva, Switzerland, Sept. 1996, pp. 158\u2013163.","key":"268970_CR29","DOI":"10.1109\/EURDAC.1996.558199"},{"key":"268970_CR30","series-title":"Technical Report UCB\/ERL","volume-title":"SIS: A system for sequential circuit synthesis","author":"E.M. Sentovich","year":"1992","unstructured":"E.M. Sentovich, K.J. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha, H. Savoj, P.R. Stephan, R.K. Brayton, and A. Sangiovanni-Vincentelli, \u201cSIS: A system for sequential circuit synthesis,\u201d Technical Report UCB\/ERL M92\/41, University of Berkeley at Berkeley, Berkeley, California, May 1992."},{"doi-asserted-by":"crossref","unstructured":"E.M. Sentovich, H. Toma, and G. Berry, \u201cLatch optimization in circuit generated from high-level description,\u201d in Proc. IEEE\/ACM ICCAD'96, San Jose, California, Nov. 1996, pp. 428\u2013435.","key":"268970_CR31","DOI":"10.1109\/ICCAD.1996.569833"},{"doi-asserted-by":"crossref","unstructured":"D. Stoffel and W. Kunz, \u201cRecord & play: A structural fixed point iteration for sequential circuit verification,\u201d in Proc. IEEE\/ACM ICCAD'97, San Jose, California, Nov. 1997, pp. 394\u2013399.","key":"268970_CR32","DOI":"10.1109\/ICCAD.1997.643566"},{"doi-asserted-by":"crossref","unstructured":"T. Tamisier, \u201cComputing the observable equivalence relation of a finite state machine,\u201d in Proc. IEEE ICCAD'93, San Jose, California, Nov. 1993, pp. 184\u2013187.","key":"268970_CR33","DOI":"10.1109\/ICCAD.1993.580053"},{"doi-asserted-by":"crossref","unstructured":"H. Touati, H. Savoj, B. Lin, R.K. Brayton, and A. Sangiovanni-Vincentelli, \u201cImplicit enumeration of finite state machines using BDDs,\u201d in Proc. IEEE ICCAD'90, San Jose, California, Nov. 1990, pp. 130\u2013133.","key":"268970_CR34","DOI":"10.1109\/ICCAD.1990.129860"},{"doi-asserted-by":"crossref","unstructured":"T. Villa, \u201cNOVA. State assignment of finite state machines for optimal two-level logic implementations,\u201d in Proc. ACM\/IEEE DAC'89, June 1989, pp. 327\u2013332.","key":"268970_CR35","DOI":"10.1145\/74382.74437"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008748802907.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008748802907\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008748802907.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:23:07Z","timestamp":1754367787000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008748802907"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,10]]},"references-count":35,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2000,10]]}},"alternative-id":["268970"],"URL":"https:\/\/doi.org\/10.1023\/a:1008748802907","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2000,10]]}}}