{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T10:40:06Z","timestamp":1740220806816,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540237389"},{"type":"electronic","value":"9783540304944"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30494-4_11","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T18:42:14Z","timestamp":1277836934000},"page":"144-158","source":"Crossref","is-referenced-by-count":3,"title":["Non-miter-based Combinational Equivalence Checking by Comparing BDDs with Different Variable Orders"],"prefix":"10.1007","author":[{"given":"In-Ho","family":"Moon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carl","family":"Pixley","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Anastasakis, D., Damiano, R., Ma, H.T., Stanion, T.: A practical and efficient method for compare-point matching. In: Proceedings of the Design Automation Conference, New Orleans, LA, June 2002, pp. 305\u2013310 (2002)","key":"11_CR1","DOI":"10.1109\/DAC.2002.1012640"},{"doi-asserted-by":"crossref","unstructured":"Berman, C.L., Trevillyan, L.H.: Functional comparison of logic designs for VLSI circuits. In: Proceedings of the International Conference on Computer-Aided Design, Santa Clara, CA, November 1989, pp. 456\u2013459 (1989)","key":"11_CR2","DOI":"10.1109\/ICCAD.1989.76990"},{"issue":"1","key":"11_CR3","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1109\/43.486279","volume":"15","author":"J. Bern","year":"1996","unstructured":"Bern, J., Meinel, C., Slobodova, A.: Global rebuilding of obdd\u2019s avoiding memory requirement maxima. IEEE Transactions on CAD\u00a015(1), 131\u2013134 (1996)","journal-title":"IEEE Transactions on CAD"},{"issue":"2","key":"11_CR4","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1016\/S0020-0190(80)90078-2","volume":"10","author":"M. Blum","year":"1980","unstructured":"Blum, M., Chandra, A., Wegman, M.: Equivalence of free boolean graphs can be decided probabilistically in polynomial time. Information Processing Letters\u00a010(2), 80\u201382 (1980)","journal-title":"Information Processing Letters"},{"unstructured":"Brand, D.: Verification of large synthesized designs. In: Proceedings of the International Conference on Computer-Aided Design, Santa Clara, CA, November 1993, pp. 534\u2013537 (1993)","key":"11_CR5"},{"issue":"8","key":"11_CR6","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"unstructured":"Cabodi, G., Quer, S., Meinel, C., Sack, H., Slobodova, A., Stangier, C.: Binary decision diagrams and the multiple variable order problem. In: International Workshop on Logic Synthesis, Lake Tahoe, CA (May 1998)","key":"11_CR7"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1007\/3-540-08860-1_17","volume-title":"Automata, Languages and Programming","author":"S. Fortune","year":"1978","unstructured":"Fortune, S., Hopcroft, J., Schmidt, E.: The complexity of equivalence and containment for free single variable program schemes. In: Ausiello, G., B\u00f6hm, C. (eds.) ICALP 1978. LNCS, vol.\u00a062, pp. 227\u2013240. Springer, Heidelberg (1978)"},{"doi-asserted-by":"crossref","unstructured":"Fujii, H., Ootomo, G., Hori, C.: Interleaving based variable ordering methods for ordered binary decision diagrams. In: Proceedings of the International Conference on Computer-Aided Design, Santa Clara, CA, November 1993, pp. 38\u201341 (1993)","key":"11_CR9","DOI":"10.1109\/ICCAD.1993.580028"},{"doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Krohm, F.: Equivalence checking using cuts and heaps. In: Proceedings of the Design Automation Conference, Anaheim, CA, June 1997, pp. 263\u2013268 (1997)","key":"11_CR10","DOI":"10.1145\/266021.266090"},{"issue":"12","key":"11_CR11","doi-asserted-by":"crossref","first-page":"1377","DOI":"10.1109\/TCAD.2002.804386","volume":"21","author":"A. Kuehlmann","year":"2002","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property checking. IEEE Transactions on CAD\u00a021(12), 1377\u20131394 (2002)","journal-title":"IEEE Transactions on CAD"},{"doi-asserted-by":"crossref","unstructured":"Kwak, H.H., Moon, I.-H., Kukula, J., Shiple, T.: Combinational equivalence checking through function transformation. In: Proceedings of the International Conference on Computer-Aided Design, San Jose, CA (November 2002)","key":"11_CR12","DOI":"10.1145\/774572.774650"},{"issue":"5","key":"11_CR13","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on CAD\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Transactions on CAD"},{"doi-asserted-by":"crossref","unstructured":"Matsunaga, Y.: An efficient equivalence checker for combinational circuits. In: Proceedings of the Design Automation Conference, June 1996, pp. 629\u2013634 (1996)","key":"11_CR14","DOI":"10.1145\/240518.240637"},{"doi-asserted-by":"crossref","unstructured":"Mohnke, J., Malik, S.: Permutation and phase independent boolean comparison. In: Proceedings of the European Conference on Design Automation, Paris, France, February 1993, pp. 86\u201392 (1993)","key":"11_CR15","DOI":"10.1109\/EDAC.1993.386495"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/3-540-36126-X_4","volume-title":"Formal Methods in Computer-Aided Design","author":"I.-H. Moon","year":"2002","unstructured":"Moon, I.-H., Kwak, H.H., Kukula, J., Shiple, T., Pixley, C.: Simplifying circuits for formal verification using parametric representation. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 52\u201368. Springer, Heidelberg (2002)"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/3-540-44585-4_12","volume-title":"Computer Aided Verification","author":"J. Moondanos","year":"2001","unstructured":"Moondanos, J., Seger, C.-J.H., Hanna, Z., Kaiss, D.: Clever: Divide and conquer combinational logic equivalence verification with false negative elimination. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 131\u2013143. Springer, Heidelberg (2001)"},{"doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the Design Automation Conference, June 2001, pp. 530\u2013535 (2001)","key":"11_CR18","DOI":"10.1145\/378239.379017"},{"issue":"1-2","key":"11_CR19","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1023\/A:1008349024680","volume":"16","author":"J. Park","year":"2000","unstructured":"Park, J., Burns, M., Pixley, C., Cho, H.: An efficient logic checker for industrial circuits. Journal of Electronic Testing\u00a016(1-2), 91\u2013106 (2000)","journal-title":"Journal of Electronic Testing"},{"unstructured":"Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of the International Conference on Computer-Aided Design, Santa Clara, CA, November 1993, pp. 42\u201347 (1993)","key":"11_CR20"},{"doi-asserted-by":"crossref","unstructured":"Scholl, C., Becker, B., Brogle, A.: Multiple variable order problem for binary decision diagrams: Theory and practical application. In: Proceedings of the Asia and South Pacific Design Automation Conference, February 2001, pp. 85\u201390 (2001)","key":"11_CR21","DOI":"10.1145\/370155.370284"},{"unstructured":"Stanion, T.: Circuit synthesis verification method and apparatus. U.S. Patent 6,056,784 (May 2000)","key":"11_CR22"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30494-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T09:57:10Z","timestamp":1740218230000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30494-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540237389","9783540304944"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30494-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}