{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:30:12Z","timestamp":1755217812225,"version":"3.43.0"},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2002,7,1]],"date-time":"2002-07-01T00:00:00Z","timestamp":1025481600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,7,1]],"date-time":"2002-07-01T00:00:00Z","timestamp":1025481600000},"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":[[2002,7]]},"DOI":"10.1023\/a:1016096020556","type":"journal-article","created":{"date-parts":[[2002,12,28]],"date-time":"2002-12-28T20:59:24Z","timestamp":1041109164000},"page":"95-101","source":"Crossref","is-referenced-by-count":1,"title":["Efficient Combinational Verification Using Overlapping Local BDDs and a Hash Table"],"prefix":"10.1007","volume":"21","author":[{"given":"Rajarshi","family":"Mukherjee","sequence":"first","affiliation":[]},{"given":"Jawahar","family":"Jain","sequence":"additional","affiliation":[]},{"given":"Koichiro","family":"Takayama","sequence":"additional","affiliation":[]},{"given":"Jacob A.","family":"Abraham","sequence":"additional","affiliation":[]},{"given":"Donald S.","family":"Fussell","sequence":"additional","affiliation":[]},{"given":"Masahiro","family":"Fujita","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5087922_CR1","doi-asserted-by":"crossref","unstructured":"C.L. Berman and L.H. Trevyllian, \u201cFunctional comparison of logic designs for VLSI circuits,\u201d in ICCAD, 1989, pp. 456-459.","DOI":"10.1109\/ICCAD.1989.76990"},{"key":"5087922_CR2","unstructured":"D. Brand, \u201cVerification of large synthesized designs,\u201d in ICCAD, 1993, pp. 534-537."},{"issue":"8","key":"5087922_CR3","doi-asserted-by":"crossref","first-page":"667","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant, \u201cGraph-based algorithms for Boolean function manipulation,\u201d IEEE Transactions on Computers, Vol. C-35, No. 8, pp. 667-691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"5087922_CR4","doi-asserted-by":"crossref","unstructured":"E. Cerny and C. Mauras, \u201cTautology checking using cross-controllability and cross-observability relations,\u201d in ICCAD, 1990, pp. 34-38.","DOI":"10.1109\/ICCAD.1990.129833"},{"key":"5087922_CR5","doi-asserted-by":"crossref","unstructured":"S.A. Cook, \u201cThe complexity of theorem proving procedures,\u201d in 3rd ACM SIGACT, 1971, pp. 151-158.","DOI":"10.1145\/800157.805047"},{"key":"5087922_CR6","unstructured":"M. Fujita, H. Fujisawa, and N. Kawato, \u201cEvaluation and improvements of Boolean comparison method based on binary decision diagrams,\u201d in ICCAD, 1988, pp. 2-5."},{"key":"5087922_CR7","doi-asserted-by":"crossref","unstructured":"J. Jain, R. Mukherjee, and M. Fujita, \u201cAdvanced verification techniques based on learning,\u201d in 32nd Design Automation Conf., June 1995, pp. 420-426.","DOI":"10.1109\/DAC.1995.249984"},{"key":"5087922_CR8","doi-asserted-by":"crossref","unstructured":"W. Kunz, \u201cHANNIBAL: An efficient tool for logic verification based on recursive learning,\u201d in ICCAD, 1993, pp. 538-543.","DOI":"10.1109\/ICCAD.1993.580111"},{"key":"5087922_CR9","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1145\/357062.357071","volume":"1","author":"T. Lengauer","year":"1979","unstructured":"T. Lengauer and R. Tarjan, \u201cA fast algorithm for finding dominators in a flowgraph,\u201d ACM Transactions on Programming Languages, Vol. 1, pp. 121-141, 1979.","journal-title":"ACM Transactions on Programming Languages"},{"key":"5087922_CR10","unstructured":"S. Malik, A. Wang, R. Brayton, and A. Sangiovanni-Vincentelli, \u201cLogic verification using binary decision diagrams in a logic synthesis environment,\u201d in ICCAD, 1988, pp. 6-9."},{"key":"5087922_CR11","doi-asserted-by":"crossref","unstructured":"Y. Matsunaga, \u201cAn efficient equivalence checker for combinational circuits,\u201d in DAC, 1996, pp. 629-634.","DOI":"10.1109\/DAC.1996.545651"},{"key":"5087922_CR12","doi-asserted-by":"crossref","unstructured":"R. Mukherjee, J. Jain, and M. Fujita, \u201cVERIFUL: VERIfication using FUnctional learning,\u201d in European Design and Test Conf., March 1995, pp. 444-448.","DOI":"10.1109\/EDTC.1995.470358"},{"key":"5087922_CR13","unstructured":"R. Mukherjee, J. Jain, M. Fujita, J. Abraham, and D. Fussell, \u201cObservations on verification techniques based on learning,\u201d in IWLS, 1995."},{"key":"5087922_CR14","doi-asserted-by":"crossref","unstructured":"R. Mukherjee, J. Jain, K. Takayama, M. Fujita, J. Abraham, and D. Fussell, \u201cEfficient combinational verifi-cation using BDDs and a hash table,\u201d in ISCAS, 1997, pp. 1025-1028.","DOI":"10.1109\/ISCAS.1997.621909"},{"key":"5087922_CR15","doi-asserted-by":"crossref","unstructured":"S. Reddy, W. Kunz, and D.K. Pradhan, \u201cNovel verification framework combining structural and OBDD methods in a synthesis environment,\u201d in 32nd Design Automation Conf., June 1995, pp. 414-419.","DOI":"10.1109\/DAC.1995.249983"},{"key":"5087922_CR16","unstructured":"R. Rudell, \u201cDynamic variable ordering for ordered binary decision diagrams,\u201d in ICCAD, 1993, pp. 42-47."},{"key":"5087922_CR17","unstructured":"\u201cSIS: A system for sequential circuit synthesis,\u201d Report M92\/41, University of California, Berkeley, 1992."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1016096020556.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1016096020556\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1016096020556.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T20:21:14Z","timestamp":1754425274000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1016096020556"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,7]]},"references-count":17,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,7]]}},"alternative-id":["5087922"],"URL":"https:\/\/doi.org\/10.1023\/a:1016096020556","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2002,7]]}}}