{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,21]],"date-time":"2025-04-21T04:44:10Z","timestamp":1745210650345},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540001164"},{"type":"electronic","value":"9783540361268"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36126-x_4","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:55:19Z","timestamp":1269885319000},"page":"52-69","source":"Crossref","is-referenced-by-count":10,"title":["Simplifying Circuits for Formal Verification Using Parametric Representation"],"prefix":"10.1007","author":[{"given":"In-Ho","family":"Moon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hee Hwan","family":"Kwak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Kukula","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Shiple","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carl","family":"Pixley","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,11,5]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"M. Aagaard, R. B. Jones, and C.-J. H. Seger. Formal verification using parametric representations of boolean constraints. In Proceedings of the Design Automation Conference, pages 402\u2013407, June 1999.","DOI":"10.1145\/309847.309968"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"C. L. Berman and L. H. Trevillyan. Functional comparison of logic designs for VLSI circuits. In Proceedings of the International Conference on Computer-Aided Design, pages 456\u2013459, Santa Clara, CA, November 1989.","DOI":"10.1109\/ICCAD.1989.76990"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"D. Brand. Verification of large synthesized designs. In Proceedings of the International Conference on Computer-Aided Design, pages 534\u2013537, Santa Clara, CA, November 1993.","DOI":"10.1109\/ICCAD.1993.580110"},{"issue":"8","key":"4_CR4","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, August 1986.","journal-title":"IEEE Transactions on Computers"},{"issue":"5","key":"4_CR5","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1109\/T-C.1974.223967","volume":"C-23","author":"E. Cerny","year":"1974","unstructured":"E. Cerny and M. A. Marin. A computer algorithm for the synthesis of memoryless logic circuits. IEEE Transactions on Computers, C-23(5):455\u2013465, May 1974.","journal-title":"IEEE Transactions on Computers"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"E. Cerny and C. Mauras. Tautology checking using cross-controllability and cross-observability relations. In Proceedings of the International Conference on Computer-Aided Design, pages 34\u201337, Santa Clara, CA, November 1990.","DOI":"10.1109\/ICCAD.1990.129833"},{"key":"4_CR7","unstructured":"O. Coudert, C. Berthet, and J. C. Madre. Verification of sequential machines using Boolean functional vectors. In L. Claesen, editor, Proceedings IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, pages 111\u2013128, Leuven, Belgium, November1989."},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"O. Coudert and J. C. Madre. A unified framework for the formal verification of sequential circuits. In Proceedings of the International Conference on Computer-Aided Design, pages 126\u2013129, November 1990.","DOI":"10.1109\/ICCAD.1990.129859"},{"issue":"8","key":"4_CR9","doi-asserted-by":"crossref","first-page":"1005","DOI":"10.1109\/43.298036","volume":"13","author":"P. Jain","year":"1994","unstructured":"P. Jain and G. Gopalakrishnan. Efficient symbolic simulation-based verifiaction using the parametric form of boolean expressions. IEEE Transactions on CAD, 13(8): 1005\u20131015, August 1994.","journal-title":"IEEE Transactions on CAD"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"A. Kuehlmann and F. Krohm. Equivalence checking using cuts and heaps. In Proceedings of the Design Automation Conference, pages 263\u2013268, Anaheim, CA, June 1997.","DOI":"10.1109\/DAC.1997.597155"},{"key":"4_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/10722167_12","volume-title":"12th Conference on Computer Aided Verification (CAV\u201900)","author":"J. H. Kukula","year":"2000","unstructured":"J. H. Kukula and T. R. Shiple. Building circuits from relations. In E. A. Emerson and A. P. Sistla, editors, 12th Conference on Computer Aided Verification (CAV\u201900), pages 131\u2013143. Springer-Verlag, Chicago, July 2000. LNCS 1855."},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"H. H. Kwak, I.-H. Moon, J. Kukula, and T. Shiple. Combinational equivalence checking through function transformation. In Proceedings of the International Conference on Computer-Aided Design (To appear), San Jose, CA, November 2002.","DOI":"10.1145\/774572.774650"},{"issue":"5","key":"4_CR13","first-page":"506","volume":"48","author":"J. P. Marques-Silva","year":"1999","unstructured":"J. P. Marques-Silva and K. A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on CAD, 48(5):506\u2013521, May 1999.","journal-title":"IEEE Transactions on CAD"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Y. Matsunaga. An efficient equivalence checker for combinational circuits. In Proceedings of the Design Automation Conference, pages 629\u2013634, June 1996.","DOI":"10.1145\/240518.240637"},{"key":"4_CR15","volume-title":"Symbolic Model Checking","author":"K. L. McMillan","year":"1994","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1994."},{"key":"4_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/3-540-40922-X_6","volume-title":"Formal Methods in Computer Aided Design","author":"I.-H. Moon","year":"2000","unstructured":"I.-H. Moon, G. D. Hachtel, and F. Somenzi. Border-block triangular form and conjunction schedule in image computation. InW. A. Hunt, Jr. and S. D. Johnson, editors, Formal Methods in Computer Aided Design, pages 73\u201390. Springer-Verlag, November 2000. LNCS 1954."},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"I.-H. Moon, J. H. Kukula, K. Ravi, and F. Somenzi. To split or to conjoin: The question in image computation. In Proceedings of the Design Automation Conference, pages 23\u201328, Los Angeles, CA, June 2000.","DOI":"10.1145\/337292.337305"},{"key":"4_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/3-540-44585-4_12","volume-title":"13th Conference on Computer Aided Verification (CAV\u201901)","author":"J. Moondanos","year":"2001","unstructured":"J. Moondanos, C.-J. H. Seger, Z. Hanna, and D. Kaiss. Clever: Divide and conquer combinational logic equivalence verification with false negative elimination. In B. Berry, H. Comon, and A. Finkel, editors, 13th Conference on Computer Aided Verification (CAV\u201901), pages 131\u2013143. Springer-Verlag, Paris, July 2001. LNCS 2101."},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the Design Automation Conference, pages 530\u2013535, June 2001.","DOI":"10.1145\/378239.379017"}],"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\/3-540-36126-X_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,25]],"date-time":"2021-10-25T04:28:32Z","timestamp":1635136112000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36126-X_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001164","9783540361268"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-36126-x_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}