{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T05:18:47Z","timestamp":1736227127218,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540619376"},{"type":"electronic","value":"9783540495673"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0031825","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:59:01Z","timestamp":1134284341000},"page":"419-434","source":"Crossref","is-referenced-by-count":6,"title":["Decomposition techniques for efficient ROBDD construction"],"prefix":"10.1007","author":[{"given":"Jawahar","family":"Jain","sequence":"first","affiliation":[]},{"given":"Amit","family":"Narayan","sequence":"additional","affiliation":[]},{"given":"A.","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[]},{"given":"C.","family":"Coelho","sequence":"additional","affiliation":[]},{"given":"R. K.","family":"Brayton","sequence":"additional","affiliation":[]},{"given":"Sunil P.","family":"Khatri","sequence":"additional","affiliation":[]},{"given":"M.","family":"Fujita","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"key":"30_CR1","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"C-27","author":"S. B. Akers","year":"1978","unstructured":"Sheldon B. Akers. Binary decision diagrams. IEEE Transactions on Computers, C-27:509\u2013516, June 1978.","journal-title":"IEEE Transactions on Computers"},{"key":"30_CR2","doi-asserted-by":"crossref","unstructured":"C. L. Berman. Circuit width, register allocation, and ordered binary decision diagrams. IEEE Transactions on Computer-Aided Design, pages 1059\u20131066, August 1991.","DOI":"10.1109\/43.85742"},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"K. S. Brace, R. L. Rudell, and R. E. Bryant. Efficient Implementation of a BDD Package. In DAC, pages 40\u201345, June 1990.","DOI":"10.1145\/123186.123222"},{"key":"30_CR4","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. Bryant","year":"1986","unstructured":"R. Bryant. Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35:677\u2013691, August 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"30_CR5","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 Computing Surveys, 24:293\u2013318, September 1992.","journal-title":"ACM Computing Surveys"},{"key":"30_CR6","unstructured":"G. Cabodi and P. Camurati. Symbolic fsm traversais based on the transition relation. submitted to Transaction on Computer-Aided Design, 1994."},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, and Stefano Quer. Auxiliary variables for extending symbolic traversal techniques to data paths. 31st DAC, pages 289\u2013293, June 1994.","DOI":"10.1145\/196244.196380"},{"key":"30_CR8","doi-asserted-by":"crossref","unstructured":"O. Coudert, C. Berthet, and J. C. Madre. Verification of Sequential Machines Based on Symbolic Execution. In Proc. of the Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, 1989.","DOI":"10.1007\/3-540-52148-8_30"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"S. Malik et. al. Logic Verification using Binary Decision Diagrams in a Logic Synthesis Environment. In ICCAD, pages 6\u20139, November 1988.","DOI":"10.1109\/ICCAD.1988.122451"},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"M. Fujita, H. Fujisawa, and N. Kawato. Evaluation and improvements of Boolean comparison method based on binary decision diagrams. ICCAD, pages 2\u20135, November 1988.","DOI":"10.1109\/ICCAD.1988.122450"},{"key":"30_CR11","volume-title":"Technical Report UCB\/ERL M93\/58","author":"R. Hojati","year":"1993","unstructured":"R. Hojati, S.C. Krishnan, and R. K. Brayton. Heuristic Algorithms for Early Quantification and Partial Product Minimization. Technical Report UCB\/ERL M93\/58, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, July 1993."},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"J. Jain, J. Bitner, D. S. Fussell, and J. A. Abraham. Probabilistic verification of Boolean functions. Formal Methods in System Design, 1, July 1992.","DOI":"10.1007\/BF00464357"},{"key":"30_CR13","unstructured":"J. Jain, J. Bitner, M. Abadir, D. S. Fussell, and J. A. Abraham. Indexed BDDs: Algorithmic Advances in Techniques to Represent and Verify Boolean functions. to appear in IEEE Transactions on Computers."},{"key":"30_CR14","doi-asserted-by":"crossref","unstructured":"S.-W. Jeong, B. Plessier, G. Hachtel, and F. Somenzi. Extended BDDs: Trading Canonicity for Structure in Verification Algorithms. In ICCAD, pages 464\u2013467, November 1991.","DOI":"10.1109\/ICCAD.1991.185305"},{"key":"30_CR15","doi-asserted-by":"crossref","first-page":"985","DOI":"10.1002\/j.1538-7305.1959.tb01585.x","volume":"38","author":"C. Y. Lee","year":"1959","unstructured":"C. Y. Lee. Representation of switching circuits by binary-decision programs. Bell Syst. Tech. J., 38:985\u2013999, 1959.","journal-title":"Bell Syst. Tech. J."},{"key":"30_CR16","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. A fast algorithm for finding dominators in a flowgraph. ACM Transactions on Programming Languages, 1:121\u2013141, July 1979.","journal-title":"ACM Transactions on Programming Languages"},{"key":"30_CR17","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic model checking: An approach to the state explosion problem. Ph.D Thesis, Dept. of Computer Sciences, Carnegie Mellon University, 1992.","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"30_CR18","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"30_CR19","unstructured":"A. Narayan, S. P. Khatri, J. Jain, M. Fujita, R. K. Brayton, and A. Sangiovanni-Vincentelli. A Study of Composition Schemes for Mixed Apply\/Compose Based Construction of ROBDDs. In Intl. Conf. on VLSI Design, January 1996."},{"key":"30_CR20","doi-asserted-by":"crossref","unstructured":"A. Narayan, J. Jain, M. Fujita, and A. L. Sangiovanni-Vincentelli. Partitioned-ROBDDs \u2014 A Compact, Canonical and Efficiently Manipulable Representation for Boolean Functions. ICCAD, November 1996. To appear.","DOI":"10.1109\/ICCAD.1996.569909"},{"key":"30_CR21","unstructured":"R. L. Rudell. Dynamic Variable Ordering for Ordered Binary Decision Diagrams In ICCAD, pages 42\u201347, November 1993."},{"key":"30_CR22","volume-title":"Technical Report UCB\/ERL M92\/41","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. L. Sangiovanni-Vincentelli. SIS: A System for Sequential Circuit Synthesis. Technical Report UCB\/ERL M92\/41, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, May 1992."},{"key":"30_CR23","doi-asserted-by":"crossref","unstructured":"H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. Implicit State Enumeration of Finite State Machines using BDD's. In ICCAD, pages 130\u2013133, November 1990.","DOI":"10.1109\/ICCAD.1990.129860"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0031825","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,6]],"date-time":"2025-01-06T12:10:58Z","timestamp":1736165458000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0031825"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540619376","9783540495673"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/bfb0031825","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}