{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,23]],"date-time":"2026-01-23T17:43:22Z","timestamp":1769190202232,"version":"3.49.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2011,12,1]],"date-time":"2011-12-01T00:00:00Z","timestamp":1322697600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","award":["1361.001 and 1444.001"],"award-info":[{"award-number":["1361.001 and 1444.001"]}],"id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF-0702668"],"award-info":[{"award-number":["CCF-0702668"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Reconfigurable Technol. Syst."],"published-print":{"date-parts":[[2011,12]]},"abstract":"<jats:p>We describe an optimization method for combinational and sequential logic networks, with emphasis on scalability. The proposed resynthesis (a) is capable of substantial logic restructuring, (b) is customizable to solve a variety of optimization tasks, and (c) has reasonable runtime on industrial designs. The approach uses don't-cares computed for a window surrounding a node and can take into account external don't-cares (e.g., unreachable states). It uses a SAT solver for all aspects of Boolean manipulation: computing don't-cares for a node in the window, and deriving a new Boolean function of the node after resubstitution. Experimental results on 6-input LUT networks after a high effort synthesis show substantial reductions in area and delay. When applied to 20 large academic benchmarks, the LUT counts and logic levels are reduced by 45.0% and 12.2%, respectively. The longest runtime for synthesis and mapping is about two minutes. When applied to a set of 14 industrial benchmarks ranging up to 83K 6-LUTs, the LUT counts and logic levels are reduced by 11.8% and 16.5%, respectively. The longest runtime is about 30 minutes.<\/jats:p>","DOI":"10.1145\/2068716.2068720","type":"journal-article","created":{"date-parts":[[2011,12,27]],"date-time":"2011-12-27T15:22:22Z","timestamp":1324999342000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":63,"title":["Scalable don't-care-based logic optimization and resynthesis"],"prefix":"10.1145","volume":"4","author":[{"given":"Alan","family":"Mishchenko","sequence":"first","affiliation":[{"name":"University of California, Berkeley, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Brayton","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jie-Hong R.","family":"Jiang","sequence":"additional","affiliation":[{"name":"National Taiwan University, Taipei, Taiwan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephen","family":"Jang","sequence":"additional","affiliation":[{"name":"Xilinx Inc., Sunnyvale, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,12,28]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Altera Corp. 2011. Altera Stratix IV FPGA family overview. http:\/\/www.altera.com\/products\/devices\/stratix-fpgas\/stratix-iv\/overview\/stxiv-overview.html.  Altera Corp. 2011. Altera Stratix IV FPGA family overview. http:\/\/www.altera.com\/products\/devices\/stratix-fpgas\/stratix-iv\/overview\/stxiv-overview.html."},{"key":"e_1_2_1_2_1","volume-title":"ABC: A system for sequential synthesis and verification, release 80802","author":"Berkeley Verification and Synthesis Research Group (BVSRG).","year":"2011","unstructured":"Berkeley Verification and Synthesis Research Group (BVSRG). 2011 . ABC: A system for sequential synthesis and verification, release 80802 . http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/. Berkeley Verification and Synthesis Research Group (BVSRG). 2011. ABC: A system for sequential synthesis and verification, release 80802. http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/."},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Betz V. Rose J. and Marquardt A. 1999. Architecture and CAD for Deep-Submicron FPGAs. Kluwer Academic Publishers.   Betz V. Rose J. and Marquardt A. 1999. Architecture and CAD for Deep-Submicron FPGAs. Kluwer Academic Publishers.","DOI":"10.1007\/978-1-4615-5145-4"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD'00)","volume":"1954","author":"Bjesse P.","unstructured":"Bjesse , P. and Claessen , K . 2000. SAT-Based verification without state space traversal . In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD'00) . Lecture Notes in Computer Science , vol. 1954 , Springer, 372--389. Bjesse, P. and Claessen, K. 2000. SAT-Based verification without state space traversal. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD'00). Lecture Notes in Computer Science, vol. 1954, Springer, 372--389."},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the International Workshop on Logic and Synthesis (IWLS'06)","author":"Case M. L.","year":"2006","unstructured":"Case , M. L. , Mishchenko , A. , and Brayton , R. K . 2006. Inductively finding a reachable state space over-approximation . In Proceedings of the International Workshop on Logic and Synthesis (IWLS'06) . 172--179. http:\/\/www.eecs.berkeley.edu\/~alanmi\/publications\/ 2006 \/iwls06_inv.pdf. Case, M. L., Mishchenko, A., and Brayton, R. K. 2006. Inductively finding a reachable state space over-approximation. In Proceedings of the International Workshop on Logic and Synthesis (IWLS'06). 172--179. http:\/\/www.eecs.berkeley.edu\/~alanmi\/publications\/2006\/iwls06_inv.pdf."},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the International Workshop on Logic and Synthesis (IWLS'08)","author":"Case M. L.","year":"2008","unstructured":"Case , M. L. , Mishchenko , A. , and Brayton , R. K . 2008. Cut-Based inductive invariant computation . In Proceedings of the International Workshop on Logic and Synthesis (IWLS'08) . 253--258. http:\/\/www.eecs. berkeley.edu\/~alanmi\/publications\/ 2008 \/iwls08_ind.pdf. Case, M. L., Mishchenko, A., and Brayton, R. K. 2008. Cut-Based inductive invariant computation. In Proceedings of the International Workshop on Logic and Synthesis (IWLS'08). 253--258. http:\/\/www.eecs. berkeley.edu\/~alanmi\/publications\/2008\/iwls08_ind.pdf."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2007.358111"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the Design Automation and Test in Europe Conference (DATE'92)","author":"Chen K.-C.","unstructured":"Chen , K.-C. and Cong , J . 1992. Maximal reduction of lookup-table-based FPGAs . In Proceedings of the Design Automation and Test in Europe Conference (DATE'92) . 224--229. Chen, K.-C. and Cong, J. 1992. Maximal reduction of lookup-table-based FPGAs. In Proceedings of the Design Automation and Test in Europe Conference (DATE'92). 224--229."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382677"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/503048.503060"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the SAT'03 Conference. http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\/.","author":"Een E.","unstructured":"Een , E. and S\u00f6rensson , N . 2003. An extensible SAT-solver . In Proceedings of the SAT'03 Conference. http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\/. Een, E. and S\u00f6rensson, N. 2003. An extensible SAT-solver. In Proceedings of the SAT'03 Conference. http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\/."},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the Design Automation and Test in Europe Conference (DATE'03)","author":"Goldberg E.","unstructured":"Goldberg , E. and Novikov , Y . 2003. Verification of proofs of unsatisfiability for CNF formulas . In Proceedings of the Design Automation and Test in Europe Conference (DATE'03) . 886--891. Goldberg, E. and Novikov, Y. 2003. Verification of proofs of unsatisfiability for CNF formulas. In Proceedings of the Design Automation and Test in Europe Conference (DATE'03). 886--891."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996691"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the International Conference on Computer Aided Design (ICCAD'07)","author":"Lee C.-C.","year":"2007","unstructured":"Lee , C.-C. , Jiang , J.-H. R. , Huang , C.-Y. , and Mishchenko , A . 2007. Scalable exploration of functional dependency by interpolation and incremental SAT solving . In Proceedings of the International Conference on Computer Aided Design (ICCAD'07) . 227--233. http:\/\/www.eecs.berkeley.edu\/~alanmi\/publications\/ 2007 \/iccad07_fd.pdf. Lee, C.-C., Jiang, J.-H. R., Huang, C.-Y., and Mishchenko, A. 2007. Scalable exploration of functional dependency by interpolation and incremental SAT solving. In Proceedings of the International Conference on Computer Aided Design (ICCAD'07). 227--233. http:\/\/www.eecs.berkeley.edu\/~alanmi\/publications\/2007\/iccad07_fd.pdf."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the International Workshop on Logic and Synthesis (IWLS'05)","author":"McMillan K.","year":"2005","unstructured":"McMillan , K. 2005 . Don't-Care computation using k-clause approximation . In Proceedings of the International Workshop on Logic and Synthesis (IWLS'05) . 153--160. McMillan, K. 2005. Don't-Care computation using k-clause approximation. In Proceedings of the International Workshop on Logic and Synthesis (IWLS'05). 153--160."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.378353"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2005.264"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the International Workshop on Logic and Synthesis (IWLS'06)","author":"Mishchenko A.","year":"2006","unstructured":"Mishchenko , A. and Brayton , R . 2006. Scalable logic synthesis using a simple circuit structure . In Proceedings of the International Workshop on Logic and Synthesis (IWLS'06) . 15--22. http:\/\/www.eecs. berkeley.edu\/~alanmi\/publications\/ 2006 \/iwls06_sls.pdf. Mishchenko, A. and Brayton, R. 2006. Scalable logic synthesis using a simple circuit structure. In Proceedings of the International Workshop on Logic and Synthesis (IWLS'06). 15--22. http:\/\/www.eecs. berkeley.edu\/~alanmi\/publications\/2006\/iwls06_sls.pdf."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1147048"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.860955"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1233501.1233679"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2006.887925"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the International Conference on Computer-Aided Design (ICCAD'07)","author":"Mishchenko A.","year":"2007","unstructured":"Mishchenko , A. , Cho , S. , Chatterjee , S. , and Brayton , R . 2007b. Combinational and sequential mapping with priority cuts . In Proceedings of the International Conference on Computer-Aided Design (ICCAD'07) . http:\/\/www.eecs.berkeley.edu\/~alanmi\/publications\/ 2007 \/iccad07_map.pdf. Mishchenko, A., Cho, S., Chatterjee, S., and Brayton, R. 2007b. Combinational and sequential mapping with priority cuts. In Proceedings of the International Conference on Computer-Aided Design (ICCAD'07). http:\/\/www.eecs.berkeley.edu\/~alanmi\/publications\/2007\/iccad07_map.pdf."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1509456.1509477"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1508128.1508152"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the International Conference on Computer-Aided Design (ICCAD'08)","author":"Mishchenko A.","unstructured":"Mishchenko , A. , Case , M. L. , Brayton , R. , and Jang , S . 2008b. Scalable and scalably-verifiable sequential synthesis . In Proceedings of the International Conference on Computer-Aided Design (ICCAD'08) . 234--241. Mishchenko, A., Case, M. L., Brayton, R., and Jang, S. 2008b. Scalable and scalably-verifiable sequential synthesis. In Proceedings of the International Conference on Computer-Aided Design (ICCAD'08). 234--241."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.35836"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/275107.275118"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2007.358021"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996688"},{"key":"e_1_2_1_33_1","volume-title":"SIS: A system for sequential circuit synthesis. Tech. rep. UCB\/ERI, M92\/41, ERL, Department of EECS","author":"Sentovich E.","year":"1992","unstructured":"Sentovich , E. , Singh , K. J. , Lavagno , L. , Moon , C. , Murgai , R. , 1992 . SIS: A system for sequential circuit synthesis. Tech. rep. UCB\/ERI, M92\/41, ERL, Department of EECS , University of California , Berkeley. Sentovich, E., Singh, K. J., Lavagno, L., Moon, C., Murgai, R., et al. 1992. SIS: A system for sequential circuit synthesis. Tech. rep. UCB\/ERI, M92\/41, ERL, Department of EECS, University of California, Berkeley."},{"key":"e_1_2_1_34_1","unstructured":"Xilinx Corp. 2011. Xilinx Virtex-5 product table. http:\/\/www.xilinx.com\/products\/silicon_solutions\/fpgas\/virtex\/virtex5\/v5product_table.pdf.  Xilinx Corp. 2011. Xilinx Virtex-5 product table. http:\/\/www.xilinx.com\/products\/silicon_solutions\/fpgas\/virtex\/virtex5\/v5product_table.pdf."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2007.358019"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1146970"}],"container-title":["ACM Transactions on Reconfigurable Technology and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2068716.2068720","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2068716.2068720","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:54:24Z","timestamp":1750240464000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2068716.2068720"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12]]},"references-count":35,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011,12]]}},"alternative-id":["10.1145\/2068716.2068720"],"URL":"https:\/\/doi.org\/10.1145\/2068716.2068720","relation":{},"ISSN":["1936-7406","1936-7414"],"issn-type":[{"value":"1936-7406","type":"print"},{"value":"1936-7414","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,12]]},"assertion":[{"value":"2009-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-12-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}