{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:34:42Z","timestamp":1770273282038,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,2,12]],"date-time":"2023-02-12T00:00:00Z","timestamp":1676160000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,2,12]]},"DOI":"10.1145\/3543622.3573196","type":"proceedings-article","created":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T23:15:13Z","timestamp":1676070913000},"page":"27-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Eliminating Excessive Dynamism of Dataflow Circuits Using Model Checking"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7172-6720","authenticated-orcid":false,"given":"Jiahui","family":"Xu","sequence":"first","affiliation":[{"name":"ETH Z\u00fcrich, Z\u00fcrich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3126-7379","authenticated-orcid":false,"given":"Emmet","family":"Murphy","sequence":"additional","affiliation":[{"name":"ETH Z\u00fcrich, Z\u00fcrich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8114-250X","authenticated-orcid":false,"given":"Jordi","family":"Cortadella","sequence":"additional","affiliation":[{"name":"UPC Barcelona, Barcelona, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6659-8533","authenticated-orcid":false,"given":"Lana","family":"Josipovic","sequence":"additional","affiliation":[{"name":"ETH Z\u00fcrich, Z\u00fcrich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,2,12]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"657","volume-title":"CA","author":"Cortadella J.","year":"2006","unstructured":"J. Cortadella, M. Kishinevsky, and B. Grundmann, \"Synthesis of synchronous elastic architectures,\" in Proceedings of the 43rd Design Automation Conference, San Francisco, CA, Jul. 2006, pp. 657--62."},{"key":"e_1_3_2_1_2_1","first-page":"361","volume-title":"CA","author":"Carloni L. P.","year":"2000","unstructured":"L. P. Carloni and A. L. Sangiovanni-Vincentelli, \"Performance analysis and optimization of latency insensitive systems,\" in Proceedings of the 37th Design Automation Conference, Los Angeles, CA, Jun. 2000, pp. 361--67."},{"key":"e_1_3_2_1_3_1","first-page":"177","volume-title":"TX","author":"Budiu M.","year":"2005","unstructured":"M. Budiu, P. V. Artigas, and S. C. Goldstein, \"Dataflow: A complement to superscalar,\" in Proceedings of the IEEE International Symposium on Performance Analysis of Systems and Software, Austin, TX, Mar. 2005, pp. 177--86."},{"key":"e_1_3_2_1_4_1","first-page":"127","volume-title":"CA","author":"Josipovic L.","year":"2018","unstructured":"L. Josipovic, R. Ghosal, and P. Ienne, \"Dynamically scheduled high-level synthesis,\" in Proceedings of the 26th ACM\/SIGDA International Symposium on Field Programmable Gate Arrays, Monterey, CA, Feb. 2018, pp. 127--36."},{"key":"e_1_3_2_1_5_1","first-page":"288","volume-title":"CA","author":"Cheng J.","year":"2020","unstructured":"J. Cheng, L. Josipovic, G. A. Constantinides, P. Ienne, and J. Wickerson, \"Combining dynamic & static scheduling in high-level synthesis,\" in Proceedings of the 28th ACM\/SIGDA International Symposium on Field Programmable Gate Arrays, Seaside, CA, Feb. 2020, pp. 288--98."},{"key":"e_1_3_2_1_6_1","first-page":"162","volume-title":"CA","author":"Josipovic L.","year":"2019","unstructured":"L. Josipovic, A. Guerrieri, and P. Ienne, \"Speculative dataflow circuits,\" in Proceedings of the 27th ACM\/SIGDA International Symposium on Field Programmable Gate Arrays, Seaside, CA, Feb. 2019, pp. 162--71."},{"key":"e_1_3_2_1_7_1","first-page":"1","volume-title":"New York","author":"Josipovic L.","year":"2022","unstructured":"L. Josipovic, A. Marmet, A. Guerrieri, and P. Ienne, \"Resource sharing in dataflow circuits,\" in Proceedings of the 30th IEEE Symposium on Field-Programmable Custom Computing Machines, New York, May 2022, pp. 1--9."},{"key":"e_1_3_2_1_8_1","first-page":"186","volume-title":"CA","author":"Josipovic L.","year":"2020","unstructured":"L. Josipovic, S. Sheikhha, A. Guerrieri, P. Ienne, and J. Cortadella, \"Buffer placement and sizing for high-performance dataflow circuits,\" in Proceedings of the 28th ACM\/SIGDA International Symposium on Field Programmable Gate Arrays, Seaside, CA, Feb. 2020, pp. 186--96."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/307988.307989"},{"key":"e_1_3_2_1_10_1","first-page":"419","volume-title":"Symbolic model checking,\" in Computer Aided Verification","author":"Edmund C.","year":"1996","unstructured":"C. Edmund, K. McMillan, S. Campos, and V. Hartonas-Garmhausen, \"Symbolic model checking,\" in Computer Aided Verification, Berlin, Heidelberg, Jun. 1996, pp. 419--22."},{"key":"e_1_3_2_1_11_1","first-page":"353","volume-title":"Pacific Grove","author":"Clarke E.","year":"1989","unstructured":"E. Clarke, D. Long, and K. McMillan, \"Compositional model checking,\" in Proceedings of the Fourth Annual Symposium on Logic in computer science, Pacific Grove, California, USA, Jun. 1989, pp. 353--362."},{"key":"e_1_3_2_1_12_1","first-page":"81","article-title":"Compositional reasoning in model checking,\" in Compositionality","author":"Berezin S.","year":"1998","unstructured":"S. Berezin, S. Campos, and E. M. Clarke, \"Compositional reasoning in model checking,\" in Compositionality: The Significant Difference, May 1998, pp. 81--102.","journal-title":"The Significant Difference"},{"key":"e_1_3_2_1_13_1","first-page":"1250","volume-title":"Automation and Test in Europe Conference and Exhibition","author":"Verma A. K.","year":"2008","unstructured":"A. K. Verma, P. Brisk, and P. Ienne, \"Variable latency speculative addition: A new paradigm for arithmetic circuit design,\" in Proceedings of the Design, Automation and Test in Europe Conference and Exhibition, Munich, Mar. 2008, pp. 1250--55."},{"key":"e_1_3_2_1_14_1","unstructured":"The LLVM Compiler Infrastructure 2018. [Online]. Available: http:\/\/www.llvm. org"},{"issue":"5","key":"e_1_3_2_1_15_1","first-page":"1","article-title":"Brisk, and P. Ienne","volume":"16","author":"L.","year":"2017","unstructured":"L. Josipovi\", P. Brisk, and P. Ienne, \"An out-of-order load-store queue for spatial computing,\" ACM Transactions on Embedded Computing Systems, vol. 16, no. 5s, pp. 125:1--125:19, Sep. 2017.","journal-title":"An out-of-order load-store queue for spatial computing,\" ACM Transactions on Embedded Computing Systems"},{"key":"e_1_3_2_1_16_1","first-page":"24","article-title":"ABC: An academic industrial-strength verification tool,\" in Computer Aided Verification, Berlin","author":"Brayton R.","year":"2010","unstructured":"R. Brayton and A. Mishchenko, \"ABC: An academic industrial-strength verification tool,\" in Computer Aided Verification, Berlin, Heidelberg, 2010, pp. 24--40.","journal-title":"Heidelberg"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/MCAS.2021.3071631"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7458595"},{"key":"e_1_3_2_1_19_1","first-page":"1","volume-title":"CA","author":"Josipovic L.","year":"2020","unstructured":"L. Josipovic, A. Guerrieri, and P. Ienne, \"Dynamatic: From C\/C to dynamically scheduled circuits,\" in Proceedings of the 28th ACM\/SIGDA International Symposium on Field Programmable Gate Arrays, Seaside, CA, Feb. 2020, pp. 1--10."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"The nuXmv symbolic model checker,\" in Computer Aided Verification","author":"Cavada R.","year":"2014","unstructured":"R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta, \"The nuXmv symbolic model checker,\" in Computer Aided Verification, Vienna, Austria, Jul. 2014, pp. 334--42."},{"key":"e_1_3_2_1_21_1","unstructured":"Vivado Design Suite Xilinx Inc. 2020. [Online]. Available: https:\/\/docs.xilinx. com\/v\/u\/2019.2-English\/ug901-vivado-synthesis"},{"key":"e_1_3_2_1_22_1","first-page":"375","volume-title":"UK","author":"Rizzi C.","year":"2022","unstructured":"C. Rizzi, A. Guerrieri, P. Ienne, and L. Josipovic, \"A comprehensive timing model for accurate frequency tuning in dataflow circuits,\" in Proceedings of the 22nd International Conference on Field-Programmable Logic and Applications, Belfast, UK, Aug. 2022, pp. 375--83."},{"key":"e_1_3_2_1_23_1","volume-title":"Polybench: The polyhedral benchmark suite","author":"Pouchet L.-N.","year":"2012","unstructured":"L.-N. Pouchet, Polybench: The polyhedral benchmark suite, 2012. [Online]. Available: http:\/\/www.cs.ucla.edu\/pouchet\/software\/polybench"},{"key":"e_1_3_2_1_24_1","volume-title":"NC","author":"Reagen B.","year":"2014","unstructured":"B. Reagen, R. Adolf, Y. S. Shao, G.-Y.Wei, and D. Brooks, \"MachSuite: Benchmarks for accelerator design and customized architectures,\" in Proceedings of the IEEE International Symposium on Workload Characterization, Raleigh, NC, October 2014."},{"key":"e_1_3_2_1_25_1","unstructured":"Mentor Graphics \"ModelSim \" 2016. [Online]. Available: https:\/\/www.mentor. com\/products\/fv\/modelsim\/"},{"key":"e_1_3_2_1_26_1","first-page":"197","volume-title":"Tianjin","author":"Josipovic L.","year":"2019","unstructured":"L. Josipovic, A. Bhattacharyya, A. Guerrieri, and P. Ienne, \"Shrink it or shed it! Minimize the use of LSQs in dataflow designs,\" in Proceedings of the IEEE International Conference on Field Programmable Technology, Tianjin, Dec. 2019, pp. 197--205."},{"key":"e_1_3_2_1_27_1","volume-title":"Xilinx Inc., 2018","author":"Suite User Guide Vivado Design","year":"2017","unstructured":"Vivado Design Suite User Guide: High-Level Synthesis, Xilinx Inc., 2018. [Online]. Available: https:\/\/www.xilinx.com\/support\/documentation\/sw_manuals\/ xilinx2017_4\/ug902-vivado-high-level-synthesis.pdf"},{"key":"e_1_3_2_1_28_1","first-page":"253","volume-title":"UK","author":"Elakhras A.","year":"2022","unstructured":"A. Elakhras, A. Guerrieri, L. Josipovic, and P. Ienne, \"Unleashing parallelism in elastic circuits with faster token delivery,\" in Proceedings of the 22nd International Conference on Field-Programmable Logic and Applications, Belfast, UK, Aug. 2022, pp. 253--61."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.945302"},{"key":"e_1_3_2_1_30_1","first-page":"175","volume-title":"Vienna","author":"Edwards S. A.","year":"2017","unstructured":"S. A. Edwards, R. Townsend, and M. A. Kim, \"Compositional dataflow circuits,\" in Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, Vienna, Sep. 2017, pp. 175--84."},{"key":"e_1_3_2_1_31_1","first-page":"76","volume-title":"TX","author":"Townsend R.","year":"2017","unstructured":"R. Townsend, M. A. Kim, and S. A. Edwards, \"From functional programs to pipelined dataflow circuits,\" in Proceedings of the 26th International Conference on Compiler Construction, Austin, TX, Feb. 2017, pp. 76--86."},{"key":"e_1_3_2_1_32_1","first-page":"347","volume-title":"Yasmine Hammamet","author":"Spars\u00f8 J.","year":"2009","unstructured":"J. Spars\u00f8, \"Current trends in high-level synthesis of asynchronous circuits,\" in Proceedings of the 16th IEEE International Conference on Electronics, Circuits, and Systems, Yasmine Hammamet, Dec. 2009, pp. 347--50."},{"key":"e_1_3_2_1_33_1","first-page":"219","volume-title":"May 2021","author":"Herklotz Y.","unstructured":"Y. Herklotz, Z. Du, N. Ramanathan, and J. Wickerson, \"An empirical study of the reliability of high-level synthesis tools,\" in 2021 IEEE 29th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM), May 2021, pp. 219--23."},{"key":"e_1_3_2_1_34_1","first-page":"315","volume-title":"Apr. 2019","author":"Faissole F.","unstructured":"F. Faissole, G. A. Constantinides, and D. Thomas, \"Formalizing loop-carried dependencies in Coq for high-level synthesis,\" in 2019 IEEE 27th Annual International Symposium on Field-Programmable Custom Computing Machines, Apr. 2019, pp. 315--15."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2021.3066466"},{"key":"e_1_3_2_1_36_1","first-page":"195","volume-title":"May 2021","author":"Cheng J.","unstructured":"J. Cheng, J. Wickerson, and G. A. Constantinides, \"Probabilistic scheduling in high-level synthesis,\" in 2021 IEEE 29th Annual International Symposium on Field- Programmable Custom Computing Machines, May 2021, pp. 195--203."},{"key":"e_1_3_2_1_37_1","first-page":"219","volume-title":"CA","author":"Najibi M.","year":"2013","unstructured":"M. Najibi and P. A. Beerel, \"Slack matching mode-based asynchronous circuits for average-case performance,\" in Proceedings of the 32nd International Conference on Computer-Aided Design, San Jose, CA, Nov. 2013, pp. 219--25."},{"key":"e_1_3_2_1_38_1","first-page":"362","volume-title":"CA","author":"Bufistov D.","year":"2007","unstructured":"D. Bufistov, J. Cortadella, M. Kishinevsky, and S. Sapatnekar, \"A general model for performance optimization of sequential systems,\" in Proceedings of the International Conference on Computer-Aided Design, San Jose, CA, Nov. 2007, pp. 362--69."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065579.1065796"}],"event":{"name":"FPGA '23: The 2023 ACM\/SIGDA International Symposium on Field Programmable Gate Arrays","location":"Monterey CA USA","acronym":"FPGA '23","sponsor":["SIGDA ACM Special Interest Group on Design Automation"]},"container-title":["Proceedings of the 2023 ACM\/SIGDA International Symposium on Field Programmable Gate Arrays"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3543622.3573196","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3543622.3573196","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:48Z","timestamp":1750186848000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3543622.3573196"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,2,12]]},"references-count":39,"alternative-id":["10.1145\/3543622.3573196","10.1145\/3543622"],"URL":"https:\/\/doi.org\/10.1145\/3543622.3573196","relation":{},"subject":[],"published":{"date-parts":[[2023,2,12]]},"assertion":[{"value":"2023-02-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}