{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:25:09Z","timestamp":1787592309512,"version":"build-2736575974"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>\n                    This paper proposes a mechanized formal semantics for\n                    <jats:italic toggle=\"yes\">dataflow<\/jats:italic>\n                    circuits: rather than following a predetermined, static schedule, the execution of the circuit components is constrained solely by the availability of their input data. We model circuit components as abstract computing units, asynchronously connected with each other through unidirectional, unbounded FIFO. In contrast to Kahn\u2019s classic, denotational semantic framework, our semantics is operational. It intends to reflect Dennis\u2019 dataflow paradigm with firing, while still formalizing the observable behaviors of circuits as channels histories.\n                  <\/jats:p>\n                  <jats:p>The components we handle are either stateless or stateful, and may be non-deterministic. We formalize sufficient conditions to achieve the determinacy of circuits executions: all possible schedules of such circuits lead to a unique observable behavior. We provide two equivalent views for circuits. The first one is a direct and natural representation as graphs of components. The second is a core, structured term calculus, which enables constructing and reasoning about circuits in a inductive way. We prove that both representations are semantically equivalent.<\/jats:p>\n                  <jats:p>We conduct our formalization within the Coq proof assistant. We experimentally validate its relevance by applying our general semantic framework to dataflow circuits generated with Dynamatic, a recent HLS tool exploiting dataflow circuits to generate dynamically scheduled, elastic circuits.<\/jats:p>","DOI":"10.1145\/3720432","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"507-533","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A Mechanized Semantics for Dataflow Circuits"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-6412-3181","authenticated-orcid":false,"given":"Tony","family":"Law","sequence":"first","affiliation":[{"name":"Univ Rennes - Inria - CNRS - IRISA, Rennes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7029-3297","authenticated-orcid":false,"given":"Delphine","family":"Demange","sequence":"additional","affiliation":[{"name":"Univ Rennes - Inria - CNRS - IRISA, Rennes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0189-0223","authenticated-orcid":false,"given":"Sandrine","family":"Blazy","sequence":"additional","affiliation":[{"name":"Univ Rennes - Inria - CNRS - IRISA, Rennes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"Lennart Augustsson Jacob Schwartz and Rishiyur S Nikhil. 2001. Bluespec Language Definition. Sandburst Corp (2001)."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"G\u00e9rard Berry and Lionel Rieg. 2022. Towards Coq-verified Esterel Semantics and Compiling. doi:10.48550\/arXiv.1909.12582 arXiv:1909.12582 [cs]","DOI":"10.48550\/arXiv.1909.12582"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385965"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371112"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_24"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(88)90016-0"},{"key":"e_1_3_2_8_2","unstructured":"M. Budiu and S. Goldstein. 2002. Pegasus: An Efficient Intermediate Representation."},{"key":"e_1_3_2_9_2","unstructured":"P. L. Campbell K. Krishna and R. A. Ballance. 1993. Refining and Defining the Program Dependence Web. (May 1993)."},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2009.2030436"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41641"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","unstructured":"Jianyi Cheng Lana Josipovi\u0107 George A. Constantinides and John Wickerson. 2022. Dynamic Inter-Block Scheduling for HLS. In 2022 32nd International Conference on Field-Programmable Logic and Applications (FPL). 243\u2013252. doi:10.1109\/FPL57034.2022.00045","DOI":"10.1109\/FPL57034.2022.00045"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Jianyi Cheng John Wickerson and George A. Constantinides. 2021. Probabilistic Scheduling in High-Level Synthesis. In 2021 IEEE 29th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM). 195\u2013203. doi:10.1109\/FCCM51124.2021.00031","DOI":"10.1109\/FCCM51124.2021.00031"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3110268"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1147077"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1980.1653418"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7{_}145"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/642089.642111"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"W. Dosch. 2005. Designing Combinational Circuits with List Homomorphisms. In Third ACIS Int\u2019l Conference on Software Engineering Research Management and Applications (SERA\u201905). 288\u2013297. doi:10.1109\/SERA.2005.35","DOI":"10.1109\/SERA.2005.35"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3274280"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3626202.3637556"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.5555\/901184"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-6345-1_34"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485494"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3174243.3174264"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2021.3105574"},{"key":"e_1_3_2_27_2","unstructured":"Gilles Kahn. 1974. The Semantics of a Simple Language for Parallel Programming. (1974)."},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1137\/0114108"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Tony Law Delphine Demange and Sandrine Blazy. 2025. A Mechanized Semantics for Dataflow Circuits. doi:10.5281\/zenodo.14938628","DOI":"10.5281\/zenodo.14938628"},{"key":"e_1_3_2_30_2","unstructured":"Tony Law Delphine Demange and Sandrine Blazy. 2025. A Mechanized Semantics for Dataflow Circuits \u2013 Appendix. https:\/\/dl.acm.org\/doi\/10.1145\/3720432#supplementary-materials"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/TASSP.1986.1164809"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.381846"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","unstructured":"Edward A. Lee and Eleftherios Matsikoudis. 2009. The Semantics of Dataflow with Firing. In From Semantics to Computer Science (1 ed.) Yves Bertot G\u00e9rard Huet Jean-Jacques L\u00e9vy and Gordon Plotkin (Eds.). Cambridge University Press 71\u201371. doi:10.1017\/CBO9780511770524.005","DOI":"10.1017\/CBO9780511770524.005"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511770524.006"},{"key":"e_1_3_2_36_2","unstructured":"Mentor Graphics. 2020. ModelSim."},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Patrick Meredith Michael Katelman Jos\u00e9 Meseguer and Grigore Ro\u015fu. 2010. A Formal Executable Semantics of Verilog. In Eighth ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010). 179\u2013188. doi:10.1109\/MEMCOD.2010.5558634","DOI":"10.1109\/MEMCOD.2010.5558634"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511770524.018"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/2670529.2754970"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.5555\/888568"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96742"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.3233\/FI-1995-22128"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0479-7"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11265-015-0971-y"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.5555\/911362"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3543622.3573196"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720432","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720432","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:30:51Z","timestamp":1787589051000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720432"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":45,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720432"],"URL":"https:\/\/doi.org\/10.1145\/3720432","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}