{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,5]],"date-time":"2024-12-05T06:10:25Z","timestamp":1733379025392,"version":"3.30.1"},"reference-count":34,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2001,2,1]],"date-time":"2001-02-01T00:00:00Z","timestamp":980985600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Systems Architecture"],"published-print":{"date-parts":[[2001,2]]},"DOI":"10.1016\/s1383-7621(00)00064-3","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T20:00:10Z","timestamp":1027627210000},"page":"163-179","source":"Crossref","is-referenced-by-count":2,"title":["Reachability analysis of large circuits using disjunctive partitioning and partial iterative squaring"],"prefix":"10.1016","volume":"47","author":[{"given":"Gianpiero","family":"Cabodi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paolo","family":"Camurati","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Quer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1383-7621(00)00064-3_BIB1","doi-asserted-by":"crossref","unstructured":"C. Pixley, A computational theory and implementation of sequential hardware equivalence, in: AMS\/DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 3, 1991, pp. 293\u2013320","DOI":"10.1007\/BFb0023719"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB2","doi-asserted-by":"crossref","unstructured":"C. Pixley, G. Beihl, Calculating resetability and reset sequences, in: Proceedings of IEEE ICCAD'91, San Jose, CA, November 1991, pp. 376\u2013379","DOI":"10.1109\/ICCAD.1991.185280"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB3","doi-asserted-by":"crossref","unstructured":"C. Pixley, S.W. Jeong, G.D. Hachtel, Exact calculation of synchronization sequences based on binary decision diagrams, in: Proceedings of ACM\/IEEE DAC'92, June 1992, pp. 614\u2013619","DOI":"10.1109\/DAC.1992.227811"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB4","doi-asserted-by":"crossref","unstructured":"B. Lin, H.J. Touati, A. Richard Newton, Don't care minimization of multi-level sequential logic networks, in: Proceedings of IEEE ICCAD'90, San Jose, CA, November 1990, pp. 414\u2013417","DOI":"10.1109\/ICCAD.1990.129940"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB5","doi-asserted-by":"crossref","unstructured":"B. Lin, A. Richard Newton, Implicit manipulation of equivalence classes using binary decision diagrams, in: Proceedings of IEEE ICCD'91, October 1991, pp. 81\u201385","DOI":"10.1109\/ICCD.1991.139995"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB6","doi-asserted-by":"crossref","unstructured":"T. Tamisier, Computing the observable equivalence relation of a finite state machine, in: Proceedings of IEEE ICCAD'93, San Jose, CA, November 1993, pp. 184\u2013187","DOI":"10.1109\/ICCAD.1993.580053"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB7","doi-asserted-by":"crossref","unstructured":"H. Touati, H. Savoj, B. Lin, R.K. Brayton, A. Sangiovanni-Vincentelli, Implicit enumeration of finite state machines using BDDs, in: Proceedings of IEEE ICCAD'90, San Jose, CA, November 1990, pp. 130\u2013133","DOI":"10.1109\/ICCAD.1990.129860"},{"issue":"4","key":"10.1016\/S1383-7621(00)00064-3_BIB8","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1109\/43.275352","article-title":"Symbolic model checking for sequential circuit verification","volume":"13","author":"Burch","year":"1994","journal-title":"IEEE Transactions on CAD"},{"issue":"7","key":"10.1016\/S1383-7621(00)00064-3_BIB9","doi-asserted-by":"crossref","first-page":"935","DOI":"10.1109\/43.238030","article-title":"Redundancy identification\/removal and test generation for sequential circuits using implicit state enumeration","volume":"12","author":"Cho","year":"1993","journal-title":"IEEE Transactions on CAD"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB10","doi-asserted-by":"crossref","unstructured":"J. Moondanos, J. Abraham, Sequential redundancy identification using verification techniques, in: Proceedings of IEEE ITC'92, September 1992, pp. 197\u2013205","DOI":"10.1109\/TEST.1992.527820"},{"issue":"8","key":"10.1016\/S1383-7621(00)00064-3_BIB11","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for Boolean function manipulation","volume":"35","author":"Bryant","year":"1986","journal-title":"IEEE Transactions on Computers C"},{"issue":"3","key":"10.1016\/S1383-7621(00)00064-3_BIB12","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","article-title":"Symbolic Boolean manipulation with ordered binary-decision diagrams","volume":"24","author":"Bryant","year":"1992","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB13","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, L.J. Hwang, Symbolic model checking: 1020 states and beyond, in: Proceedings of IEEE LICS'90, Symposium on Logic in Computer Science, June 1990, pp. 428\u2013439","DOI":"10.1109\/LICS.1990.113767"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB14","doi-asserted-by":"crossref","unstructured":"R. Rudell, Dynamic variable ordering for ordered binary decision diagrams, in: Proceedings of IEEE\/ACM ICCAD'93, San Jose, CA, November 1993, pp. 42\u201347","DOI":"10.1109\/ICCAD.1993.580029"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB15","unstructured":"D.E. Long, Model checking, abstraction, and compositional verification, Ph.D. thesis, Carnegie Mellon University, July 1993"},{"year":"1994","series-title":"Computer Aided Verification of Coordinating Processes","author":"Kurshan","key":"10.1016\/S1383-7621(00)00064-3_BIB16"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB17","doi-asserted-by":"crossref","unstructured":"K. Ravi, F. Somenzi, High-density reachability analysis, in: Proceedings of IEEE\/ACM ICCAD'95, San Jose, CA, November 1995, pp. 154\u2013158","DOI":"10.1109\/ICCAD.1995.480006"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB18","doi-asserted-by":"crossref","unstructured":"K. Ravi, K.L. McMillan, T.R. Shiple, F. Somenzi, Approximation and decomposition of binary decision diagram, in: Proceedings of EDA\/SIGDA\/ACM\/IEEE DAC'98, San Francisco, CA, June 1998, pp. 445\u2013450","DOI":"10.1145\/277044.277168"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB19","doi-asserted-by":"crossref","unstructured":"K. Ravi, F. Somenzi, Efficient fixpoint computation for invariant checking, in: Proceedings of IEEE ICCD'99, Austin, TX, October 1999, pp. 467\u2013474","DOI":"10.1109\/ICCD.1999.808582"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB20","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, S. Quer, Efficient state space pruning in symbolic backward traversal, in: Proceedings of IEEE ICCD'94, Cambridge, MA, October 1994, pp. 230\u2013235","DOI":"10.1109\/ICCD.1994.331895"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB21","doi-asserted-by":"crossref","first-page":"1137","DOI":"10.1016\/S1383-7621(00)00014-X","article-title":"Symbolic forward\/backward traversals of large finite state machines","volume":"46","author":"Cabodi","year":"2000","journal-title":"JSA Journal of System Architecture, The EUROMICRO Journal"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB22","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, S. Quer, Improved reachability analysis of large finite state machine, in: Proceedings of IEEE\/ACM ICCAD'96, San Jose, CA, November 1996, pp. 354\u2013360","DOI":"10.1109\/ICCAD.1996.569819"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB23","doi-asserted-by":"crossref","unstructured":"A. Narayan, A.J. Isles, J. Jain, R.K. Brayton, A. Sangiovanni-Vincentelli, Reachability analysis using partitioned-ROBDDs, in: Proceedings of IEEE\/ACM ICCAD'97, San Jose, CA, November 1997, pp. 388\u2013393","DOI":"10.1109\/ICCAD.1997.643565"},{"issue":"5","key":"10.1016\/S1383-7621(00)00064-3_BIB24","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1109\/43.759068","article-title":"Improving the efficiency of BDD-based operators by means of partitioning","volume":"18","author":"Cabodi","year":"1999","journal-title":"IEEE Transactions on CAD"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB25","unstructured":"M. Ganai, A. Aziz, Efficient coverage directed state space search, in: IWLS'98: IEEE International Workshop on Logic Synthesis, Lake Tahoe, CA, June 1998"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB26","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, L. Lavagno, S. Quer, Verification and synthesis of counters based on symbolic techniques, in: ED&TC'97: EDAA\/ACM\/IEEE European Design and Test Conference, March 1997, pp. 176\u2013181","DOI":"10.1109\/EDTC.1997.582355"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB27","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, L. Lavagno, S. Quer, Disjunctive partitioning and partial iterative squaring: an effective approach for symbolic traversal of large circuits, in: Proceedings of EDA\/SIGDA\/ACM\/IEEE DAC'97, Anaheim, CA, June 1997, pp. 728\u2013733","DOI":"10.1145\/266021.266355"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB28","doi-asserted-by":"crossref","unstructured":"K. Ravi, F. Somenzi, Hints to accelerate symbolic traversal, in: Correct Hardware Design and Verification Methods (CHARME'99), Berlin, September 1999, in: Lecture Notes in Computer Science, vol. 1703, Springer, Berlin, pp. 250\u2013264","DOI":"10.1007\/3-540-48153-2_19"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB29","unstructured":"H. Cho, G.D. Hatchel, E. Macii, M. Poncino, K. Ravi, F. Somenzi, Approximate finite state machine traversal: extensions and new results, in: IWLS'95: IEEE International Workshop on Logic Synthesis, Lake Tahoe, CA, May 1995"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB30","unstructured":"J. Jain, J. Bitner, J.A. Abraham, D.S. Fussel, Functional partitioning for verification and related problems, in: Brown\/MIT VLSI Conference, March 1992, pp. 210\u2013226"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB31","doi-asserted-by":"crossref","unstructured":"A. Narayan, J. Jain, M. Fujita, A. Sangiovanni-Vincentelli. Partitioned ROBDDs \u2013 a compact, canonical and efficient manipulable representation of Boolean functions, in: Proceedings of IEEE\/ACM ICCAD'96, San Jose, CA, November 1996, pp. 547\u2013554","DOI":"10.1109\/ICCAD.1996.569909"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB32","unstructured":"F. Somenzi, CUDD: CU Decision Diagram Package \u2013 Release 2.3.0, Technical Report, Department of Electrical and Computer Engineering, University of Colorado, Boulder, CO, October 1998"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB33","unstructured":"M68HC11 Reference Manual, Motorola Inc., 1991"},{"key":"10.1016\/S1383-7621(00)00064-3_BIB34","doi-asserted-by":"crossref","unstructured":"R.K. Brayton et al., VIS, in: Proceedings of FMCAD'96, Palo Alto, CA, November 1996, in: Lecture Notes in Computer Science, vol. 1166, Springer, Berlin, pp. 248\u2013256","DOI":"10.1007\/BFb0031812"}],"container-title":["Journal of Systems Architecture"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1383762100000643?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1383762100000643?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,12,5]],"date-time":"2024-12-05T05:38:59Z","timestamp":1733377139000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1383762100000643"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,2]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2001,2]]}},"alternative-id":["S1383762100000643"],"URL":"https:\/\/doi.org\/10.1016\/s1383-7621(00)00064-3","relation":{},"ISSN":["1383-7621"],"issn-type":[{"type":"print","value":"1383-7621"}],"subject":[],"published":{"date-parts":[[2001,2]]}}}