{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T15:33:51Z","timestamp":1762875231632,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,2,22]],"date-time":"2009-02-22T00:00:00Z","timestamp":1235260800000},"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":[[2009,2,22]]},"DOI":"10.1145\/1508128.1508152","type":"proceedings-article","created":{"date-parts":[[2009,2,25]],"date-time":"2009-02-25T14:46:05Z","timestamp":1235573165000},"page":"151-160","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Scalable don't-care-based logic optimization and resynthesis"],"prefix":"10.1145","author":[{"given":"Alan","family":"Mishchenko","sequence":"first","affiliation":[{"name":"UC Berkeley, Berkeley, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Brayton","sequence":"additional","affiliation":[{"name":"UC Berkeley, Berkeley, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jie-Hong Roland","family":"Jiang","sequence":"additional","affiliation":[{"name":"National Taiwan University, Taipei, Taiwan Roc"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephen","family":"Jang","sequence":"additional","affiliation":[{"name":"Xilinx Inc., San Jose, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2009,2,22]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Berkeley Logic Synthesis and Verification Group ABC: A System for Sequential Synthesis and Verification Release 80802. http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/  Berkeley Logic Synthesis and Verification Group ABC: A System for Sequential Synthesis and Verification Release 80802. http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/646186.683097"},{"key":"e_1_3_2_1_3_1","first-page":"172","volume-title":"Proc. IWLS '06","author":"Case M. L.","year":"2006","unstructured":"M. L. Case , A. Mishchenko , and R. K. Brayton , \" Inductively finding a reachable state space over-approximation \", Proc. IWLS '06 , pp. 172 -- 179 . http:\/\/www.eecs.berkeley.edu\/~alanmi\/publications\/ 2006 \/iwls06_inv.pdf M. L. Case, A. Mishchenko, and R. K. Brayton, \"Inductively finding a reachable state space over-approximation\", Proc. IWLS '06, pp. 172--179. http:\/\/www.eecs.berkeley.edu\/~alanmi\/publications\/2006\/iwls06_inv.pdf"},{"key":"e_1_3_2_1_4_1","first-page":"253","volume-title":"Proc. IWLS'08","author":"Case M. L.","year":"2008","unstructured":"M. L. Case , A. Mishchenko , and R. K. Brayton , \" Cut-based inductive invariant computation \", Proc. IWLS'08 , pp. 253 -- 258 . http:\/\/www.eecs.berkeley.edu\/~alanmi\/publications\/ 2008 \/iwls08_ind.pdf M. L. Case, A. Mishchenko, and R. K. Brayton, \"Cut-based inductive invariant computation\", Proc. IWLS'08, pp. 253--258. http:\/\/www.eecs.berkeley.edu\/~alanmi\/publications\/2008\/iwls08_ind.pdf"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2007.358111"},{"key":"e_1_3_2_1_6_1","first-page":"224","volume-title":"Proc. DATE '92","author":"Chen K.-C.","unstructured":"K.-C. Chen and J. Cong , \" Maximal reduction of lookup-table-based FPGAs \", Proc. DATE '92 , pp. 224 -- 229 . K.-C. Chen and J. Cong, \"Maximal reduction of lookup-table-based FPGAs\", Proc. DATE '92, pp. 224--229."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/503048.503060"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382677"},{"volume-title":"SAT '03","author":"Een N.","key":"e_1_3_2_1_9_1","unstructured":"N. Een and N. S\u00f6rensson , \" An extensible SAT-solver \". SAT '03 . http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\/ N. Een and N. S\u00f6rensson, \"An extensible SAT-solver\". SAT '03. http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\/"},{"key":"e_1_3_2_1_10_1","first-page":"886","volume-title":"Proc. DATE '03","author":"Goldberg E.","unstructured":"E. Goldberg and Y. Novikov , \" Verification of proofs of unsatisfiability for CNF formulas \", Proc. DATE '03 , pp. 886 -- 891 . E. Goldberg and Y. Novikov, \"Verification of proofs of unsatisfiability for CNF formulas\", Proc. DATE '03, pp. 886--891."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996691"},{"key":"e_1_3_2_1_12_1","first-page":"227","volume-title":"Proc. ICCAD '07","author":"Lee C.-C.","year":"2007","unstructured":"C.-C. Lee , J.-H. R. Jiang , C.-Y. Huang , and A. Mishchenko . \" Scalable exploration of functional dependency by interpolation and incremental SAT solving \", Proc. ICCAD '07 , pp. 227 -- 233 . http:\/\/www.eecs.berkeley.edu\/~alanmi\/publications\/ 2007 \/iccad07_fd.pdf C.-C. Lee, J.-H. R. Jiang, C.-Y. Huang, and A. Mishchenko. \"Scalable exploration of functional dependency by interpolation and incremental SAT solving\", Proc. ICCAD '07, pp. 227--233. http:\/\/www.eecs.berkeley.edu\/~alanmi\/publications\/2007\/iccad07_fd.pdf"},{"key":"e_1_3_2_1_13_1","first-page":"1","volume-title":"Proc. CAV '03","author":"McMillan K.L.","year":"2003","unstructured":"K.L. McMillan , \"Interpolation and SAT-based model checking \". Proc. CAV '03 , pp. 1 -- 13 , LNCS 2725, Springer , 2003 . K.L. McMillan, \"Interpolation and SAT-based model checking\". Proc. CAV '03, pp. 1--13, LNCS 2725, Springer, 2003."},{"key":"e_1_3_2_1_14_1","first-page":"153","volume-title":"Proc. IWLS '05","author":"McMillan K.","unstructured":"K. McMillan , \"Don't-care computation using k-clause approximation \", Proc. IWLS '05 , pp. 153 -- 160 . K. McMillan, \"Don't-care computation using k-clause approximation\", Proc. IWLS '05, pp. 153--160."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.378353"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2005.264"},{"key":"e_1_3_2_1_17_1","first-page":"15","volume-title":"Proc. IWLS '06","author":"Mishchenko A.","year":"2006","unstructured":"A. Mishchenko and R. K. Brayton , \" Scalable logic synthesis using a simple circuit structure \", Proc. IWLS '06 , pp. 15 -- 22 . http:\/\/www. eecs.berkeley.edu\/~alanmi\/publications\/ 2006 \/iwls06_sls.pdf A. Mishchenko and R. K. Brayton, \"Scalable logic synthesis using a simple circuit structure\", Proc. IWLS '06, pp. 15--22. http:\/\/www. eecs.berkeley.edu\/~alanmi\/publications\/2006\/iwls06_sls.pdf"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1147048"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.860955"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1233501.1233679"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2006.887925"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1326073.1326147"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1509456.1509477"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.35836"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/275107.275118"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2007.358021"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996688"},{"key":"e_1_3_2_1_28_1","volume-title":"UC Berkeley","author":"Savoj H.","year":"1992","unstructured":"H. Savoj . Don't cares in multi-level network optimization. Ph.D. Dissertation , UC Berkeley , May 1992 . H. Savoj. Don't cares in multi-level network optimization. Ph.D. Dissertation, UC Berkeley, May 1992."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2007.358019"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1146970"},{"key":"e_1_3_2_1_32_1","unstructured":"Xilinx Virtex-5 Product Table http:\/\/www.xilinx.com\/products\/silicon_solutions\/fpgas\/virtex\/virtex5\/v5product_table.pdf  Xilinx Virtex-5 Product Table http:\/\/www.xilinx.com\/products\/silicon_solutions\/fpgas\/virtex\/virtex5\/v5product_table.pdf"},{"key":"e_1_3_2_1_33_1","unstructured":"Xilinx Stratix IV FPGA Family Overview http:\/\/www.altera.com\/products\/devices\/stratix-fpgas\/stratix-iv\/overview\/stxiv-overview.html  Xilinx Stratix IV FPGA Family Overview http:\/\/www.altera.com\/products\/devices\/stratix-fpgas\/stratix-iv\/overview\/stxiv-overview.html"}],"event":{"name":"FPGA '09: ACM\/SIGDA International Symposium on Field Programmable Gate Arrays","sponsor":["ACM Association for Computing Machinery","SIGDA ACM Special Interest Group on Design Automation"],"location":"Monterey California USA","acronym":"FPGA '09"},"container-title":["Proceedings of the ACM\/SIGDA international symposium on Field programmable gate arrays"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1508128.1508152","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1508128.1508152","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:29:38Z","timestamp":1750253378000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1508128.1508152"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2,22]]},"references-count":32,"alternative-id":["10.1145\/1508128.1508152","10.1145\/1508128"],"URL":"https:\/\/doi.org\/10.1145\/1508128.1508152","relation":{},"subject":[],"published":{"date-parts":[[2009,2,22]]},"assertion":[{"value":"2009-02-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}