{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:52:15Z","timestamp":1750308735107,"version":"3.41.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2012,10,1]],"date-time":"2012-10-01T00:00:00Z","timestamp":1349049600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"SRC Focus Center Research Program on Functional Engineered Nano-Architectonics","award":["2003-NT-1107"],"award-info":[{"award-number":["2003-NT-1107"]}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["845650"],"award-info":[{"award-number":["845650"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2012,10]]},"abstract":"<jats:p>\n            The accepted wisdom is that combinational circuits must have\n            <jats:italic>acyclic<\/jats:italic>\n            (i.e., feed-forward) topologies. Yet simple examples suggest that this is incorrect. In fact, introducing cycles (i.e., feedback) into combinational designs can lead to significant savings in area and in delay. Prior work described methodologies for synthesizing cyclic circuits with Sum-Of-Product (SOP) and Binary-Decision Diagram (BDD)-based formulations. Recently, techniques for\n            <jats:italic>analyzing<\/jats:italic>\n            and\n            <jats:italic>mapping<\/jats:italic>\n            cyclic circuits based on Boolean satisfiability (SAT) were proposed. This article presents a SAT-based methodology for\n            <jats:italic>synthesizing<\/jats:italic>\n            cyclic dependencies. The strategy is to generate cyclic functional dependencies through a technique called Craig interpolation. Given a choice of different functional dependencies, a branch-and-bound search is performed to pick the best one. Experiments on benchmark circuits demonstrate the effectiveness of the approach.\n          <\/jats:p>","DOI":"10.1145\/2348839.2348848","type":"journal-article","created":{"date-parts":[[2012,10,18]],"date-time":"2012-10-18T13:48:27Z","timestamp":1350568107000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["The Synthesis of Cyclic Dependencies with Boolean Satisfiability"],"prefix":"10.1145","volume":"17","author":[{"given":"John D.","family":"Backes","sequence":"first","affiliation":[{"name":"University of Minnesota"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc D.","family":"Riedel","sequence":"additional","affiliation":[{"name":"University of Minnesota"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11560548_20"},{"volume-title":"Proceedings of the International Conference on Computer-Aided Design.","author":"Backes J.","key":"e_1_2_1_2_1","unstructured":"Backes , J. and Riedel , M. D . 2010. Reduction of interpolants for logic synthesis . In Proceedings of the International Conference on Computer-Aided Design. Backes, J. and Riedel, M. D. 2010. Reduction of interpolants for logic synthesis. In Proceedings of the International Conference on Computer-Aided Design."},{"volume-title":"Proceedings of the International Conference on Computer-Aided Design. 143--148","author":"Backes J.","key":"e_1_2_1_3_1","unstructured":"Backes , J. , Fett , B. , and Riedel , M. D . 2008. The analysis of cyclic circuits with Boolean satisfiability . In Proceedings of the International Conference on Computer-Aided Design. 143--148 . Backes, J., Fett, B., and Riedel, M. D. 2008. The analysis of cyclic circuits with Boolean satisfiability. In Proceedings of the International Conference on Computer-Aided Design. 143--148."},{"volume-title":"Proceedings of the S. J. Satisf. (to appear).","author":"Backes J.","key":"e_1_2_1_4_1","unstructured":"Backes , J. , Fett , B. , and Riedel , M. D . 2011. The analysis and mapping of cyclic circuits with boolean satisfiability . In Proceedings of the S. J. Satisf. (to appear). Backes, J., Fett, B., and Riedel, M. D. 2011. The analysis and mapping of cyclic circuits with boolean satisfiability. In Proceedings of the S. J. Satisf. (to appear)."},{"key":"e_1_2_1_5_1","unstructured":"Benchmarks. 2005. Benchmarks from the 2005 international workshop on logic synthesis. http:\/\/iwls.org\/iwls2005\/benchmarks.html. Benchmarks . 2005. Benchmarks from the 2005 international workshop on logic synthesis. http:\/\/iwls.org\/iwls2005\/benchmarks.html."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.52213"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.1987.1270310"},{"key":"e_1_2_1_8_1","volume-title":"-J","author":"Brzozowski J.","year":"1995","unstructured":"Brzozowski , J. and Seger , C . -J . 1995 . Asynchronous Circuits. Springer . Brzozowski, J. and Seger, C.-J. 1995. Asynchronous Circuits. Springer."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775874"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"E\u00e9n N.\n     and \n      S\u00f6rensson N\n  . \n  2003\n  . An extensible SAT-solver. In SAT E. Giunchiglia and A. Tacchella Eds. Lecture Notes in Computer Science vol. \n  2919\n  . \n  Springer 502--518. E\u00e9n N. and S\u00f6rensson N. 2003. An extensible SAT-solver. In SAT E. Giunchiglia and A. Tacchella Eds. Lecture Notes in Computer Science vol. 2919. Springer 502--518.","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382610"},{"key":"e_1_2_1_12_1","unstructured":"Katz R. 1992. Contemporary Logic Design. Benjamin\/Cummings. Katz R. 1992. Contemporary Logic Design . Benjamin\/Cummings."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/266021.266070"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.108614"},{"volume-title":"Proceedings of the International Conference on Computer-Aided Design. 227--233","author":"Lee C.-C.","key":"e_1_2_1_15_1","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. 227--233 . 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. 227--233."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.293952"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_2_1_18_1","volume-title":"et al","author":"Mishchenko A.","year":"2007","unstructured":"Mishchenko , A. et al . 2007 a. ABC : A system for sequential synthesis and verification. http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/abc.htm. Mishchenko, A. et al. 2007a. ABC: A system for sequential synthesis and verification. http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/abc.htm."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2006.887925"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.2003305"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775875"},{"volume-title":"Proceedings of the International Workshop on Logic and Synthesis.","author":"Riedel M. D.","key":"e_1_2_1_23_1","unstructured":"Riedel , M. D. and Bruck , J . 2004. Timing analysis of cyclic combinational circuits . In Proceedings of the International Workshop on Logic and Synthesis. Riedel, M. D. and Bruck, J. 2004. Timing analysis of cyclic combinational circuits. In Proceedings of the International Workshop on Logic and Synthesis."},{"key":"e_1_2_1_24_1","volume-title":"SIS: A system for sequential circuit synthesis. Tech. rep.","author":"Sentovich E. M.","year":"1992","unstructured":"Sentovich , E. M. , Singh , K. J. , Lavagno , L. , Moon , C. , Murgai , R. , Saldanha , A. , Savoj , H. , Stephan , P. R. , Brayton , R. K. , and Sangiovanni-Vincentelli , A. 1992 . SIS: A system for sequential circuit synthesis. Tech. rep. , University of California , Berkeley. Sentovich, E. M., Singh, K. J., Lavagno, L., Moon, C., Murgai, R., Saldanha, A., Savoj, H., Stephan, P. R., Brayton, R. K., and Sangiovanni-Vincentelli, A. 1992. SIS: A system for sequential circuit synthesis. Tech. rep., University of California, Berkeley."},{"key":"e_1_2_1_26_1","unstructured":"S\u00f6rensson N. and Een N. 2012. Minisat v1.13 -- A SAT solver with conflict-clause minimization. http:\/\/minisat.se\/downloads\/. S\u00f6rensson N. and Een N. 2012. Minisat v1.13 -- A SAT solver with conflict-clause minimization. http:\/\/minisat.se\/downloads\/."},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the International Conference on Computer-Aided Design. 345--348","author":"Stok L.","year":"1992","unstructured":"Stok , L. 1992 . False loops through resource sharing . In Proceedings of the International Conference on Computer-Aided Design. 345--348 . Stok, L. 1992. False loops through resource sharing. In Proceedings of the International Conference on Computer-Aided Design. 345--348."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1531542.1531622"},{"key":"e_1_2_1_29_1","volume-title":"Digital Design: Principles and Practices","author":"Wakerly J. F.","year":"2000","unstructured":"Wakerly , J. F. 2000 . Digital Design: Principles and Practices . Prentice-Hall . Wakerly, J. F. 2000. Digital Design: Principles and Practices. Prentice-Hall."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/321203.321214"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2348839.2348848","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2348839.2348848","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:22:02Z","timestamp":1750278122000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2348839.2348848"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,10]]}},"alternative-id":["10.1145\/2348839.2348848"],"URL":"https:\/\/doi.org\/10.1145\/2348839.2348848","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2012,10]]},"assertion":[{"value":"2011-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}