{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2021,12,16]],"date-time":"2021-12-16T14:46:24Z","timestamp":1639665984552},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540627906","type":"print"},{"value":"9783540685197","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0035377","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T10:28:40Z","timestamp":1138184920000},"page":"4-18","source":"Crossref","is-referenced-by-count":2,"title":["Manipulation algorithms for K*BMDs"],"prefix":"10.1007","author":[{"given":"Rolf","family":"Drechsler","sequence":"first","affiliation":[]},{"given":"Bernd","family":"Becker","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Ruppertz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,26]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"D.P. Appenzeller and A. Kuehlmann. Formal verification of a PowerPC microprocessor. In Int'l Conf. on Comp. Design, pages 79\u201384, 1995.","DOI":"10.1109\/ICCD.1995.528794"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"L. Arditi. *bmds can delay the use of theorem proving for verifying arithmetic assembly instructions. In FMCAD, 1996.","DOI":"10.1007\/BFb0031798"},{"key":"2_CR3","unstructured":"B. Becker, R. Drechsler, and R. Enders. On the computational power of bit-level and word-level decision diagrams. In ASP Design Automation Conf., 1997."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"B. Becker, R. Drechsler, and M. Theobald. OKFDDs versus OBDDs and OFDDs. In ICALP, LNCS 944, pages 475\u2013486, 1995.","DOI":"10.1007\/3-540-60084-1_98"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"K.S. Brace, R.L. Rudell, and R.E. Bryant. Efficient implementation of a BDD package. In Design Automation Conf., pages 40\u201345, 1990.","DOI":"10.1145\/123186.123222"},{"key":"2_CR6","unstructured":"F. Brglez and H. Fujiwara. A neutral netlist of 10 combinational circuits and a target translator in fortran. In Int'l Symp. Circ. and Systems, Special Sess. on ATPG and Fault Simulation, pages 663\u2013698, 1985."},{"issue":"8","key":"2_CR7","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant. Graph \u2014 based algorithms for Boolean function manipulation. IEEE Trans. on Comp., 35(8):677\u2013691, 1986.","journal-title":"IEEE Trans. on Comp."},{"key":"2_CR8","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1109\/12.73590","volume":"40","author":"R.E. Bryant","year":"1991","unstructured":"R.E. Bryant. On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Trans. on Comp., 40:205\u2013213, 1991.","journal-title":"IEEE Trans. on Comp."},{"key":"2_CR9","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"R.E. Bryant. Symbolic boolean manipulation with ordered binary decision diagrams. ACM, Comp. Surveys, 24:293\u2013318, 1992.","journal-title":"ACM, Comp. Surveys"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"R.E. Bryant and Y.-A. Chen. Verification of arithmetic functions with binary moment diagrams. Technical report, CMU-CS-94-160, 1994.","DOI":"10.21236\/ADA281028"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"R.E. Bryant and Y.-A. Chen. Verification of arithmetic functions with binary moment diagrams. In Design Automation Conf., pages 535\u2013541, 1995.","DOI":"10.1109\/DAC.1995.250005"},{"key":"2_CR12","first-page":"1","volume":"P6","author":"E. Clarke","year":"1993","unstructured":"E. Clarke, M. Fujita, P. McGeer, K. McMillan, J. Yang, and X. Zhao. Multi terminal binary decision diagrams: An efficient data structure for matrix representation. In Int'l Workshop on Logic Synth., pages P6a:1\u201315, 1993.","journal-title":"Int'l Workshop on Logic Synth."},{"key":"2_CR13","unstructured":"E.M. Clarke, M. Fujita, and X. Zhao. Application of multi-terminal binary decision diagrams. IFIP WG 10.5 Workshop on Applications of the Reed-Muller Expansion in Circuit Design, pages 21\u201327, 1995."},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, M. Fujita, and X. Zhao. Hybrid decision diagrams \u2014 overcoming the limitations of MTBDDs and BMDs. In Int'l Conf. on CAD, pages 159\u2013163, 1995.","DOI":"10.21236\/ADA296684"},{"key":"2_CR15","unstructured":"E.M. Clarke and X. Zhao. Word level symbolic model checking \u2014 a new approach for verifying arithmetic circuits. Technical Report CMU-CS-95-161, 1995."},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"R. Drechsler and B. Becker. Dynamic minimization of OKFDDs. In Int'l Conf. on Comp. Design, pages 602\u2013607, 1995.","DOI":"10.1109\/ICCD.1995.528930"},{"key":"2_CR17","unstructured":"R. Drechsler, B. Becker, and S. Ruppertz. K*BMDs: A new data structure for verification. In European Design & Test Conf., pages 2\u20138, 1996."},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"R. Drechsler, A. Sarabi, M. Theobald, B. Becker, and M.A. Perkowski. Efficient representation and manipulation of switching functions based on Ordered Kronecker Functional Decision Diagrams. In Design Automation Conf., pages 415\u2013419, 1994.","DOI":"10.1145\/196244.196444"},{"key":"2_CR19","unstructured":"R. Drechsler, M. Theobald, and B. Becker. Fast OFDD based minimization of Fixed Polarity Reed-Muller expressions. In European Design Automation Conf., pages 2\u20137, 1994."},{"key":"2_CR20","unstructured":"R. Enders. Note on the complexity of binary moment diagram representations. IFIP WG 10.5 Workshop on Applications of the Reed-Muller Expansion in Circuit Design, pages 191\u2013197, 1995."},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"M. Fujita, H. Fujisawa, and N. Kawato. Evaluation and improvements of boolean comparison method based on binary decision diagrams. In Int'l Conf. on CAD, pages 2\u20135, 1988.","DOI":"10.1109\/ICCAD.1988.122450"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"M. Fujita, Y. Matsunaga, and T. Kakuda. On variable ordering of binary decision diagrams for the application of multi-level synthesis. In European Conf. on Design Automation, pages 50\u201354, 1991.","DOI":"10.1109\/EDAC.1991.206358"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"U. Kebschull, E. Schubert, and W. Rosenstiel. Multilevel logic synthesis based on functional decision diagrams. In European Conf. on Design Automation, pages 43\u201347, 1992.","DOI":"10.1109\/EDAC.1992.205890"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"R. Krieger, B. Becker, and R. Sinkovi\u0107. A BDD-based algorithm for computation of exact fault detection probabilities. In Int'l Symp. on Fault-Tolerant Comp., pages 186\u2013195, 1993.","DOI":"10.1109\/FTCS.1993.627322"},{"key":"2_CR25","unstructured":"Y.-T. Lai and S. Sastry. Edge-valued binary decision diagrams for multi-level hierarchical verification. In Design Automation Conf., pages 608\u2013613, 1992."},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"S. Malik, A.R. Wang, R.K. Brayton, and A.L. Sangiovanni-Vincentelli. Logic verification using binary decision diagrams in a logic synthesis environment. In Int'l Conf. on CAD, pages 6\u20139, 1988.","DOI":"10.1109\/ICCAD.1988.122451"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"S. Minato, N. Ishiura, and S. Yajima. Shared binary decision diagrams with attributed edges for efficient boolean function manipulation. In Design Automation Conf., pages 52\u201357, 1990.","DOI":"10.1145\/123186.123225"},{"key":"2_CR28","unstructured":"S. Panda and F. Somenzi. Who are the variables in your neighborhood. In Int'l Conf. on CAD, pages 74\u201377, 1995."},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"R. Rudell. Dynamic variable ordering for ordered binary decision diagrams. In Int'l Conf. on CAD, pages 42\u201347, 1993.","DOI":"10.1109\/ICCAD.1993.580029"},{"key":"2_CR30","unstructured":"P. Tafertshofer and M. Pedram. Factored edge-valued binary decision diagrams. to appear in Formal Methods in System Design, 1996."},{"key":"2_CR31","unstructured":"S. Yang. Logic synthesis and optimization benchmarks user guide. Technical Report 1\/95, Microelectronic Center of North Carolina, Jan. 1991."}],"container-title":["Tools and Algorithms for the Construction and Analysis of Systems","Lecture Notes in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0035377","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T10:39:39Z","timestamp":1555411179000},"score":1,"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540627906","9783540685197"],"references-count":31,"URL":"http:\/\/dx.doi.org\/10.1007\/bfb0035377","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"published":{"date-parts":[[1997]]}}}