{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,23]],"date-time":"2026-01-23T23:26:13Z","timestamp":1769210773502,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2008,6,8]],"date-time":"2008-06-08T00:00:00Z","timestamp":1212883200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2008,6,8]]},"DOI":"10.1145\/1391469.1391605","type":"proceedings-article","created":{"date-parts":[[2008,7,30]],"date-time":"2008-07-30T12:09:58Z","timestamp":1217419798000},"page":"540-545","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Merging nodes under sequential observability"],"prefix":"10.1145","author":[{"given":"Michael L.","family":"Case","sequence":"first","affiliation":[{"name":"University of California at Berkeley, CA and IBM Systems and Technology Group, Austin, TX"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Victor N.","family":"Kravets","sequence":"additional","affiliation":[{"name":"IBM TJ Watson Research Center, Yorktown, NY"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Mishchenko","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert K.","family":"Brayton","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,6,8]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"The IBM Experience,\" Tutorial Given at FMCAD","author":"Baumgartner J.","year":"2006","unstructured":"J. Baumgartner , \"Integrating FV Into Main-Stream Verification : The IBM Experience,\" Tutorial Given at FMCAD 2006 . J. Baumgartner, \"Integrating FV Into Main-Stream Verification: The IBM Experience,\" Tutorial Given at FMCAD 2006."},{"key":"e_1_3_2_1_2_1","volume-title":"Reducing structural bias in technology mapping,\" in ICCAD","author":"Chatterjee S.","year":"2005","unstructured":"S. Chatterjee , A. Mishchenko , R. K. Brayton , X. Wang , and T. Kam , \" Reducing structural bias in technology mapping,\" in ICCAD 2005 . S. Chatterjee, A. Mishchenko, R. K. Brayton, X. Wang, and T. Kam, \"Reducing structural bias in technology mapping,\" in ICCAD 2005."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.2005.68"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/266021.266090"},{"key":"e_1_3_2_1_5_1","unstructured":"D. Brand \"Verification of large synthesized designs \" in ICCAD 1993.   D. Brand \"Verification of large synthesized designs \" in ICCAD 1993."},{"key":"e_1_3_2_1_6_1","volume-title":"An efficient tool for logic verification based on recursive learning,\" in ICCAD","author":"Kunz W.","year":"1993","unstructured":"W. Kunz , \"HANNIBAL : An efficient tool for logic verification based on recursive learning,\" in ICCAD 1993 . W. Kunz, \"HANNIBAL: An efficient tool for logic verification based on recursive learning,\" in ICCAD 1993."},{"key":"e_1_3_2_1_7_1","volume-title":"Logic optimization and equivalence checking by implication analysis,\" in ICCAD","author":"Kunz W.","year":"1997","unstructured":"W. Kunz , D. Stoffel , and P. Menon , \" Logic optimization and equivalence checking by implication analysis,\" in ICCAD 1997 . W. Kunz, D. Stoffel, and P. Menon, \"Logic optimization and equivalence checking by implication analysis,\" in ICCAD 1997."},{"key":"e_1_3_2_1_8_1","volume-title":"Using SAT in combinational equivalence checking,\" in DATE","author":"Goldberg E.","year":"2001","unstructured":"E. Goldberg , M. R. Prasad , and R. K. Brayton , \" Using SAT in combinational equivalence checking,\" in DATE 2001 . E. Goldberg, M. R. Prasad, and R. K. Brayton, \"Using SAT in combinational equivalence checking,\" in DATE 2001."},{"key":"e_1_3_2_1_9_1","unstructured":"F. Lu L. C. Wang K. T. Cheng and R. C. Y. Huang \"A circuit SAT solver with signal correlation guided learning \" in DATE 2003.   F. Lu L. C. Wang K. T. Cheng and R. C. Y. Huang \"A circuit SAT solver with signal correlation guided learning \" in DATE 2003."},{"key":"e_1_3_2_1_10_1","unstructured":"Berkeley Logic Synthesis and Verification Group ABC: A System for Sequential Synthesis and Verification http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/  Berkeley Logic Synthesis and Verification Group ABC: A System for Sequential Synthesis and Verification http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.851997"},{"key":"e_1_3_2_1_12_1","volume-title":"Logic Synthesis,\" McGraw-Hill","author":"Devadas S.","year":"1994","unstructured":"S. Devadas , A. Ghosh , and K. Keutzer , \" Logic Synthesis,\" McGraw-Hill 1994 . S. Devadas, A. Ghosh, and K. Keutzer, \"Logic Synthesis,\" McGraw-Hill 1994."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1146970"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2007.358021"},{"key":"e_1_3_2_1_15_1","volume-title":"Retiming synchronous circuitry,\" in Algorithmica","author":"Leiserson C. E.","year":"1991","unstructured":"C. E. Leiserson and J. B. Saxe , \" Retiming synchronous circuitry,\" in Algorithmica 1991 . C. E. Leiserson and J. B. Saxe, \"Retiming synchronous circuitry,\" in Algorithmica 1991."},{"key":"e_1_3_2_1_16_1","volume-title":"SAT-based Verification without State Space Traversal,\" in FMCAD","author":"Bjesse P.","year":"2000","unstructured":"P. Bjesse and K. Claessen , \" SAT-based Verification without State Space Traversal,\" in FMCAD 2000 . P. Bjesse and K. Claessen, \"SAT-based Verification without State Space Traversal,\" in FMCAD 2000."},{"key":"e_1_3_2_1_17_1","volume-title":"Test generation for sequential circuits,\" in CAD of Integrated Circuits and Systems","author":"Ma H. K.","year":"1988","unstructured":"H. K. Ma , S. Devadas , A. R. Newton , and A. Sangiovanni-Vincentelli , \" Test generation for sequential circuits,\" in CAD of Integrated Circuits and Systems 1988 . H. K. Ma, S. Devadas, A. R. Newton, and A. Sangiovanni-Vincentelli, \"Test generation for sequential circuits,\" in CAD of Integrated Circuits and Systems 1988."},{"key":"e_1_3_2_1_18_1","volume-title":"Smart simulation using collaborative formal and simulation engines,\" in ICCAD","author":"Ho P. H.","year":"2000","unstructured":"P. H. Ho , T. Shiple , K. Harer , J. Kukula , R. Damiano , V. Bertacco , J. Taylor , and J. Long , \" Smart simulation using collaborative formal and simulation engines,\" in ICCAD 2000 . P. H. Ho, T. Shiple, K. Harer, J. Kukula, R. Damiano, V. Bertacco, J. Taylor, and J. Long, \"Smart simulation using collaborative formal and simulation engines,\" in ICCAD 2000."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/362003.362025"},{"key":"e_1_3_2_1_20_1","volume-title":"Counterexamples in Topology,\" Courier Dover Publications","author":"Steen L. A.","year":"1970","unstructured":"L. A. Steen and J. A. Seebach , \" Counterexamples in Topology,\" Courier Dover Publications 1970 , Page 34. L. A. Steen and J. A. Seebach, \"Counterexamples in Topology,\" Courier Dover Publications 1970, Page 34."},{"key":"e_1_3_2_1_21_1","volume-title":"A Survey of Recent Advances in SAT-Based Formal Verification,\" in Software Tools for Technology Transfer","author":"Prasad M. R.","year":"2005","unstructured":"M. R. Prasad , A. Biere , and A. Gupta , \" A Survey of Recent Advances in SAT-Based Formal Verification,\" in Software Tools for Technology Transfer 2005 . M. R. Prasad, A. Biere, and A. Gupta, \"A Survey of Recent Advances in SAT-Based Formal Verification,\" in Software Tools for Technology Transfer 2005."},{"key":"e_1_3_2_1_22_1","unstructured":"Niklas Een Niklas Sorensson MiniSat. http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\/  Niklas Een Niklas Sorensson MiniSat. http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\/"},{"key":"e_1_3_2_1_23_1","unstructured":"Sun Microsystems \"Processor Technology Resources - picoJava \" http:\/\/www.sun.com\/software\/communitysource\/processors\/picojava.xml  Sun Microsystems \"Processor Technology Resources - picoJava \" http:\/\/www.sun.com\/software\/communitysource\/processors\/picojava.xml"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1147048"},{"key":"e_1_3_2_1_25_1","volume-title":"Automatic Phase Abstraction for Formal Verification,\" in ICCAD","author":"Bjesse P.","year":"2005","unstructured":"P. Bjesse and J. Kukula , \" Automatic Phase Abstraction for Formal Verification,\" in ICCAD 2005 . P. Bjesse and J. Kukula, \"Automatic Phase Abstraction for Formal Verification,\" in ICCAD 2005."}],"event":{"name":"DAC '08: The 45th Annual Design Automation Conference 2008","location":"Anaheim California","acronym":"DAC '08","sponsor":["The EDA Consortium","IEEE\/CASS\/CANDE\/CEDA","SIGDA ACM Special Interest Group on Design Automation"]},"container-title":["Proceedings of the 45th annual Design Automation Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1391469.1391605","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1391469.1391605","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:58:04Z","timestamp":1750255084000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1391469.1391605"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,6,8]]},"references-count":25,"alternative-id":["10.1145\/1391469.1391605","10.1145\/1391469"],"URL":"https:\/\/doi.org\/10.1145\/1391469.1391605","relation":{},"subject":[],"published":{"date-parts":[[2008,6,8]]},"assertion":[{"value":"2008-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}