# A Mechanized Semantics for Dataflow Circuits

Tony Law, Delphine Demange, Sandrine Blazy

► To cite this version:

Tony Law, Delphine Demange, Sandrine Blazy. A Mechanized Semantics for Dataflow Circuits. SPLASH 2025 - ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity, Oct 2025, Singapore, Singapore. pp.1-29. hal-04851772

HAL Id: hal-04851772

https://hal.science/hal-04851772v1

Submitted on 6 Mar 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# A Mechanized Semantics for Dataflow Circuits

TONY LAW, Univ Rennes - Inria - CNRS - IRISA, France

DELPHINE DEMANGE, Univ Rennes - Inria - CNRS - IRISA, France

SANDRINE BLAZY, Univ Rennes - Inria - CNRS - IRISA, France

This paper proposes a mechanized formal semantics for *dataflow 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's classic, denotational semantic framework, our semantics is operational. It intends to reflect Dennis' dataflow paradigm with firing, while still formalizing the observable behaviors of circuits as channels histories.

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 an inductive way. We prove that both representations are semantically equivalent.

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.

CCS Concepts: • **Software and its engineering** → **Data flow languages; Semantics; Formal software verification**; Compilers; • **Hardware** → **Hardware description languages and compilation**.

Additional Key Words and Phrases: dataflow computation, operational semantics, formal proofs

## ACM Reference Format:

Tony Law, Delphine Demange, and Sandrine Blazy. 2025. A Mechanized Semantics for Dataflow Circuits. *Proc. ACM Program. Lang.* 9, OOPSLA1, Article 98 (April 2025), 29 pages. https://doi.org/10.1145/3720432

## 1 Introduction

In the dataflow paradigm of computation, programs are seen as graphs where nodes represent operations or computational processes, and edges represent communication channels to exchange data values between nodes. Each node is enabled when it has enough available data in its input channels. The first theoretic model for dataflow was proposed by Karp and Miller [27], although restricted to channels with fixed consumption and production rates. Since then, dataflow models have also been explored in computer architecture, with the pioneering work of Rodrigues [38], Dennis and Misunas [17] for novel computer architectures with a high degree of concurrency. In the domain of parallel programming for operating systems, Kahn's work on dataflow models is perhaps one of the most influential and established theory. Kahn networks express programs semantics as the least fixed point of a set of equations on continuous stream functions, defined over the histories of channels, i.e., the sequences of data passing in communication channels. We refer the interested readers to historical surveys [30, 33] for a comprehensive overview.

Authors' Contact Information: Tony Law, Univ Rennes - Inria - CNRS - IRISA, Rennes, France, tony.law@irisa.fr; Delphine Demange, Univ Rennes - Inria - CNRS - IRISA, Rennes, France, delphine.demange@irisa.fr; Sandrine Blazy, Univ Rennes - Inria - CNRS - IRISA, Rennes, France, sandrine.blazy@irisa.fr.

© 2025 Copyright held by the owner/author(s).

This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in *Proceedings of the ACM on Programming Languages*, https://doi.org/10.1145/3720432.
In this vast literature of dataflow models, we are interested in *dataflow circuits*. A circuit is a graph, where nodes are components, i.e., basic computing units, and where edges are unidirectional, unbounded FIFO communication channels. Reads are blocking on empty channels and writes are always non-blocking, thus allowing for a form of asynchronous communication. Components perform their computation in an atomic way, consuming data from their input channels and producing data on their output channels. Components can *fire*, i.e., trigger their computation, as soon as their input channels contain enough data. This dataflow model corresponds, roughly speaking, to Dennis's model of dataflow with *firing* [31], except that the initial proposal was imposing blocking writes on non-empty channels [15].

The work we present here is a first step of a larger project whose aim is to verify the functional correctness of a recent technique for high-level synthesis (HLS). This technique relies on elastic circuits [9, 14], whose abstract specification are asynchronous dataflow circuits. HLS provides automatic ways to compile software down into hardware: the compilation produces a custom hardware design rather than traditional assembly code. Software is written in C, or similar languages, and the design is expressed in a hardware description language, subsequently synthesized to the gate level. Traditional HLS techniques compute a static schedule of the components of the circuits. In contrast, HLS techniques based on elastic circuits allow for dynamic schedules, computed at run-time. This gives opportunities for performance improvement compared to static schedules [11, 24]. Elastic circuits also allow deferring the choice between a synchronous or an asynchronous implementation to later phases of the hardware design process [9].

The correctness of an HLS compilation schema consists in proving that the observable behavior of the generated hardware circuit is consistent with the semantics of the initial source program. While this ambitious, long term goal is out of the scope of the present paper, providing relevant abstraction layers is key to decompose a verified compilation chain, and to prove successive refinement steps. We argue that dataflow circuits are an interesting and important abstraction layer for the HLS schema we target in the future. Indeed, they play the essential role of an intermediate representation (IR), at the crossroad between a control-driven execution model at the source level, and a data-driven execution model like the one informally described for elastic circuits [9]. Considering dataflow circuits as a keystone, our work provides a mechanized, semantic model for dataflow circuits. Our dataflow circuits should be considered as a mid-level IR, which abstracts away from, e.g. communication protocol, clock cycles, and latency.

Our semantic model is deliberately *operational*, in contrast to more traditional approaches like Dataflow Process Networks [30], a restricted class of Kahn networks. Indeed, small-step operational styles of semantics have clearly demonstrated to be successfully applicable to whole compiler correctness proofs. They come with well-established techniques like inductive simulation diagrams to prove semantics preservation of compilation phases [32]. Operational semantics are also simple mental models for execution, and naturally extend to executable interpreters, so that the semantic model can be validated experimentally.

Our contributions all revolve around our semantic model for dataflow circuits. Figure 1 illustrates how they articulate with each other. The core of our semantic model is an abstract definition of elementary components. We instantiate it on the concrete components used in the Dynamic HLS tool [24]. On top of components, we define circuits with Cigr, a natural, graph-based IR for circuits. We define a second, alternate IR for circuits, called Cilan, as a core calculus of circuits terms, which allows both constructing circuits and reasoning inductively about circuits. We prove that both IR are semantically equivalent, so that properties established on one IR provably holds on the other. Finally, we implement an interpreter for Cigr, generic in the set of components, that we prove faithful to our semantics. We instantiate our generic interpreter on our formalization of Dynamic's components, and obtain an interpreter of Dynamic's dataflow circuits. This allows
<figure><img src="image_2.png" /><figcaption>Fig. 1. Architecture of our contributions. Regular arrows represent direct dependencies in definitions, bold arrows represent direct lemmas and theorems, dotted arrows represent instantiations. We prove dashed bold arrows as (transitive) consequences.</figcaption></figure>

us to compare the traces generated by our Dynamic interpreter with the traces obtained after
simulating Dynamic's produced circuits.

We formally prove several meta-properties of interest for our semantics. The first one is *parallelism*: despite its simple, sequential definition, with one component firing at each computation step, we prove that our semantics describes the parallel execution of subsets of components. Another key meta-property we want to achieve, in our context, is *determinacy*: although our model is non-deterministic in the way the computations are effectively triggered, circuits should exhibit a global, unique observable behavior. Not all dataflow circuits are determinate, and we formalize sufficient criteria on the components of a circuit that imply its determinacy. We aim at imposing as few constraints as possible on the components. In particular, we want to be able to deal with components that are either stateless or stateful, and that may be non-deterministic. To do so, we formalize sufficient fine-grained conditions on components, to ensure their usage within a circuit does not make their non-determinism observable.

Unless noted otherwise, the results we present in this paper are mechanically verified in the Coq proof assistant. Our Coq development is available as a reusable artifact [28]. In this paper, we present our formalization independently of its concrete Coq definition. The reasons are twofold. First, our work is not specific to the Coq proof assistant. Second, it makes our contributions accessible to a wider audience. In summary, we make the following contributions.

* We define an operational small-step semantics for dataflow circuits, represented as graphs of components in the Cigr IR. It reflects the atomic firing of components communicating asynchronously through unidirectional, unbounded FIFO buffers.

* We formalize conditions on components and prove semantic meta-properties (parallelism, trace determinacy) of circuits that only contain components verifying these conditions. Our conditions allow for stateless, stateful and safe usages of non-deterministic components.

* We provide an alternate IR, Cilan, in the form of a core calculus in which circuits are expressed as structured, inductive terms. We prove that it has the same semantic expressive power as Cigr. As a benefit, Cilan offers inductive reasoning principles on dataflow circuits, guided by the structure of the terms.

* To validate our semantic model for dataflow circuits, we extract an executable interpreter, that we prove faithful to Cigr's semantics. On a set of representative benchmarks, we obtain execution traces that are equivalent to the ones emitted by Dynamic's dataflow circuits.

The rest of the paper is organized as follows. Section 2 gives an overview of our semantic model on example circuits. Section 3 defines our basic components. Section 4 presents our formal
<figure><img src="image_3.png" /><figcaption>Fig. 2. Example of a simple component and a possible execution. Figure 2a is a single component that outputs on channel $\pi_r$ the maximum of two values taken from input channels $\pi_a$ and $\pi_b$. Figure 2b gives a possible evolution of the content of each channel, with three firings of the component, represented with the symbol $\frac{\d}{\d t}$. When it doesn't fire, other components in the circuit can fire. Channels are queues, with the front on the left and the rear on the right. Figure 2c gives the corresponding histories of each of the channels.</figcaption></figure>

semantics for dataflow circuits, represented as graphs of components in Cigr. Section 5 discusses the meta-properties of our semantics, relying on core conditions that we express on components, and then lift to whole circuits. Section 6 presents our alternate IR, Cilan, and illustrates its convenience for inductive reasoning on circuits. We prove in Section 7 its semantic equivalence to Cigr. Section 8 describes our experimental validation. Related work is discussed in Section 9, followed by conclusions.

## 2 Overview of our Dataflow Circuits

This section introduces some of the terminology we use throughout the paper, and illustrates our semantics for dataflow circuits on representative examples.

A *circuit* is a network of components connected by channels. A *component* is a computing unit that consumes and produces *tokens*; it exchanges tokens at its interface, made of *ports*. We distinguish *input ports*, that receive tokens, and *output ports*, that emit tokens. *Channels* are the means of communication of a circuit; they are unidirectional and transfer tokens from an output port to an input port. A circuit is *well-formed* when each input port is connected to at most one output port and vice versa. Working with well-formed circuits avoids dealing with implicit token duplication and token merging; well-formed circuits explicitly express these operations via dedicated components.

Figure 2 illustrates a single stateless component, computing the maximum of two input values. The component has two input ports and one output port, and channels attached to each of them. Assuming the component is part of a larger circuit, Fig. 2b shows the evolution, along several *steps* of execution, of the content of each of the channels. Note that we intentionally employ the word *execution step*, to avoid possible confusions with clocks, or cycles, which do not make sense at the level of our dataflow circuits. A channel is a queue, to which value tokens are added on the right end, and are taken out from the left end. Note that the component is not synchronous, in the sense that inputs token may arrive at different points in time: for instance, token 1 arrives later in $\pi_b$ than token 7 in $\pi_a$.

A component can *fire* when enough input tokens are available on its input ports, but does not necessarily fire. Indeed, our semantic model is a data-driven execution model in which the firing order is implementation-dependent [8]. In Fig. 2b, we indicate the component firings with the symbol $\frac{\d}{\d t}$. When it fires, this component consumes one input token on $\pi_a$ and $\pi_b$, computes the maximum value thereof and produces one token in its output channel $\pi_r$. This firing happens atomically. Note also that no token is consumed from $\pi_r$, which effectively leaves all produced output tokens in it. A sequence of execution steps describes, among other things, the content of each channel. To describe the observable behavior of component and circuits, we rely on the
<figure><img src="image_4.png" /><figcaption>Fig. 3. Two examples of well-formed circuits. Channels are shown as edges directed from an input port to an output port. Channels of particular interest are labeled with the meta-variable $\pi$.</figcaption></figure>

traditional notion of history [26], i.e., the sequence of tokens that pass through a channel. Figure 2c gives the histories for channels $\pi_a$, $\pi_b$ and $\pi_r$. Channels histories are more convenient to describe a global behavior, and abstract from the precise instants where tokens effectively enter and leave the channel.

Figure 3 gives two examples of well-formed circuits. The circuit in Fig. 3a outputs in $\pi_r$ the maximum of two input values, received in $\pi_a$ and $\pi_b$. This circuit implements the previous component with simpler, more basic components. A Fork component duplicates its input token on all its output ports. A Branch component transmits its input token to the one output port designated by its input (control) port, graphically represented on the side of Branch. This component is a typical example of a component that does not always produce the same number of token on its output ports. This is another source of asynchrony. A Sink component simply consumes its input token, producing nothing on its output. A Mux component always produces one token on its output port when it fires; the produced value depends on the input token. The circuit in Fig. 3b illustrates some other components we are able to deal with. The circuit decrements an input value from channel $\pi_n$, until it becomes negative, and then outputs the resulting value in channel $\pi_r$. The Merge component has two input ports and one output port. It transmits a token from either of its input ports to its output port, and here the choice is non-deterministic. In practice, designers take care of avoiding unwanted non-deterministic behaviors of Merge, e.g. by never having, simultaneously, two non-empty input channels for a Merge.

Our semantic model is generic in the set of possible components. In Section 3.3, we show how it can be instantiated to the components used in the Dynamatic HLS framework. In particular, we are able to handle components that are either stateless or stateful, and that are non-deterministic, such as the above Merge component. In addition, we formulate necessary conditions on components for a circuit to behave in a *determinate* way, i.e., regardless of the schedule of components, the circuit exhibits a single observable behavior. More precisely, we will prove that the histories of channels are independent of the schedule.

We want to emphasize that dataflow circuits, as we model them in our IR, should not be confused with hardware circuits. In particular, our semantic model abstracts from clock cycles, relies on unbounded channels, and abstracts from the handshake protocol [14] implementing the communication between components through channels. In Fig. 3, channels are graphically represented
as edges between components, directed from an output port to an input port. In particular, in our model, channels are not components per se, and it is not an issue to have cyclic connections between components: in Fig. 3b, a channel connecting the Branch and Merge does create a cycle, but this should not be considered as a combinational cycle at this level. We nevertheless do handle Buffer components, as they fit our model. These components do also interact with other components through unbounded channels.

# 3 Components: Basic Computing Units

Following the dataflow model presented by Dennis [16], we formalize the behavior of components with *firing rules*. We extend the notion of *commutative firing* [31] to explicitly support stateful components. This section introduces firing relations, formalizes well-formed components, and describes Dynamatic's components that we are able to model.

*Notations.* For a set $A$, we write $A_?$ for its extension with an empty value, thus corresponding to an option type. In $A_?$, values are written either $\langle a \rangle$ (read: “some $a$”) for an existing value $a \in A$, and $\epsilon$ (read: “none”) for the empty value. For a set $A$, we write $\tilde{A}$ for the set of lists of elements in $A$. We write $[]$ for the empty list, and $[x]$ for the list of a single element $x$.

## 3.1 Firing Relation

A *firing relation* defines the possible behaviors of a component as a set of firing rules. The signature of the firing relation is $\text{RULES} = (\vec{V}_? \times S) \times \mathcal{R} \times (\vec{V}_? \times S)$, where $\mathcal{V}$ is the set of tokens, $S$ is the set of component states. Let us ignore for the moment the role of $\mathcal{R}$. The set $S$ is specific to each component. For example, the state of Buffer component is able to store one token. For a memory controller, $S = \mathcal{V} \mapsto \mathcal{V}$ is a mapping from addresses to values. When a component is stateless, we use the dummy state value $\bullet$.

A firing rule is written $(\vec{i}, s) \to (\vec{o}, s')$ and expresses that firing makes the component step from state $s$ to $s'$, while consuming input tokens and producing output tokens accordingly to the consumption, resp. production, patterns $\vec{i}$ and $\vec{o}$. In a pattern, $\langle x \rangle$ denotes the effective consumption/production of a token, while $\epsilon$ denotes the absence of consumption/production. A pattern does not reflect the actual content of the channels when a component fires. For example, the firing rule $([\langle x \rangle; \epsilon], \bullet) \to ([\epsilon; \langle x + 1 \rangle], \bullet)$ consumes a token of value $x$ on the first input port, consumes no token on the second port, leaving it unchanged regardless of its content, produces no token on the first output port and produces a token of value $x + 1$ on the second output port.

Let us now explain the role of $\mathcal{R}$. Oftentimes, components are made of independent parts, which should not interfere. Think of a 2-port read-only memory controller as an aggregation of two independent controllers. Noninterference of independent parts of components corresponds to the notion of *commutative firings*, defined by Lee and Matsikoudis [31] as a pure semantic criterion. Here, we use $\mathcal{R}$ as a set of rule labels, tagging firing rules according to the sole part of the component they touch. We then use this label to formalize commutative firings with finer-grained, distinct notions (see Definitions 3.3 and 5.4). A firing rule with label $r \in \mathcal{R}$ is thus written $(\vec{i}, s) \xrightarrow{r} (\vec{o}, s')$. Components with no independent parts simply rely on a singleton $\mathcal{R}$ set.

Moreover, rule labels let us easily compose components into larger ones, by grouping together several components into a single one. For instance, starting from a 1-port read-only memory controller with a single firing rule $([\langle x \rangle], \text{mem}) \xrightarrow{r} ([\text{mem}[x]], \text{mem})$, one builds a 2-port read-only memory controller by aggregating two of them, distinguishing each of the independent ports with its proper rule label. So $\mathcal{R} = \{r_0, r_1\}$, and the firing relation becomes

$$([\langle x \rangle; \epsilon], \text{mem}) \xrightarrow{r_0} ([\text{mem}[x]; \epsilon], \text{mem})$$

$$([\epsilon; \langle x \rangle], \text{mem}) \xrightarrow{r_1} ([\epsilon; \text{mem}[x]], \text{mem})$$
## 3.2 Components

*Definition 3.1 (Component).* A component $c$ is a triple $(n_i, n_o, \rightarrow) \in \mathbb{N} \times \mathbb{N} \times \text{RULES}$ where $n_i$ is a number of input ports, $n_o$ is a number of output ports, and $\rightarrow$ is a firing relation. We write $|c|^{\text{in}}$ for the number of input ports of $c$, $|c|^{\text{out}}$ for its number of output ports, and we use a subscript notation $\rightarrow_c$ for its firing relation.

*Example 3.2.* The non-deterministic 2-way merge component Merge introduced in Section 2 is defined as the triple $(2, 1, \rightarrow_{\text{Merge}_2})$, where the firing relation $\rightarrow_{\text{Merge}_2}$ accounts for two cases: the component transmits a token from either its first or its second input. The firing relation thus includes the two rules $([\langle x \rangle; \epsilon], \bullet) \xrightarrow{r} \text{Merge}_2([\langle x \rangle], \bullet)$ and $([\epsilon; \langle x \rangle], \bullet) \xrightarrow{r} \text{Merge}_2([\langle x \rangle], \bullet)$.

To be well-formed, a component must satisfy two criteria. First, all of its firing rules must fully specify what happens on *exactly each* port; this essentially amounts to consider that components are dependent triples $(n_i, n_o, \rightarrow) \in \mathbb{N} \times \mathbb{N} \times ((V_2^{n_i} \times S) \times \mathcal{R} \times (V_2^{n_o} \times S))$. For instance, the previous firing rule $([\langle x \rangle; \epsilon], \bullet) \xrightarrow{r} c$ $([\epsilon; \langle x + 1 \rangle], \bullet)$ must only belong to the firing relation of a component that has exactly two input ports and two output ports, otherwise the component would not be well-formed. The second criterion constrains input/output ports relative to rule labels: intuitively, rule labels should indeed be consistent with the separation of ports they are supposed to represent. Concretely, if a firing rule labeled $r$ consumes a token at the $k$-th input port, then any other rule with a distinct label $r' \neq r$ should not consume a token at this port. A similar criterion applies to output ports. Definition 5.4 will later constrain the effects of separate rules on the state.

*Definition 3.3 (Well-formed component).* A component $(n_i, n_o, \rightarrow_c)$ is well-formed whenever all its firing rules meet the following conditions.

* Full specification of ports: for any rule $(\vec{i}, s_1) \xrightarrow{r} c(\vec{o}, s_2)$, then $|\vec{i}| = n_i$ and $|\vec{o}| = n_o$.

* Rule label separation: for any two rules $(\vec{i}, s_1) \xrightarrow{r} c(\vec{o}, s_2)$ and $(\vec{i}', s_1') \xrightarrow{r'} c(\vec{o}', s_2')$ with $r \neq r'$, we have $(\forall k, \vec{i}'[k] \neq \epsilon \Rightarrow \vec{i}[k] = \epsilon)$ and $(\forall k, \vec{o}'[k] \neq \epsilon \Rightarrow \vec{o}[k] = \epsilon)$.

In the rest of the paper, we assume working with well-formed components only. In practice, this is easily checked, and indeed satisfied by all the concrete components we have been considering.

## 3.3 Dynamatic's Components

We now describe how to instantiate our general definition of components to the components specifically used in the Dynamatic HLS tool. We formally define their respective firing rules, which makes us able to run a representative set of benchmarks, taken from Dynamatic's suite (see Section 8). Figure 4 gathers the firing rules for all components, that we explain below. We use natural numbers for rule labels, so $\mathcal{R} \subset \mathbb{N}$. Most of the components use a single rule label, in which case we use 0 as a convention. Some rules use the following notation: for any identifier $l, \vec{l}_\epsilon$ denotes a list where all elements are equal to $\epsilon$.

First, there are a number of basic components. Functional units Func$_f$ perform the arithmetic or logical operation $f$, which is either unary or binary. Component Source can only produce a 0 token on its output, it has no input and thus can always fire. To produce a constant value token different from 0, one composes a Source with a constant, unary, Func$_f$ unit. Component Sink only consumes a token on its input port, and has no output.

The second set of components handles token selection, duplication, merging and branching. MuX$_n$ is a $n$-to-1 multiplexer, transmitting a token from the input port selected by the token on its control input port. Fork$_n$ is a $n$-way fork, duplicating its single input token to all its output ports. Merge$_n$ is a $n$-way merge, transmitting a token from any input port, selected non-deterministically.
<figure><img src="image_5.png" /><figcaption>Fig. 4. Semantics of Dynamic's components</figcaption></figure>

CntrlMerge_n is a n-way control merge. This variant of the merge component has an extra output port where it emits a token containing the position of the accepted input token. Branch transmits its input token to only one of its output ports, depending on the token on its control input port.

Finally, we handle two types of stateful components: buffers, and memory controllers. Buffer is used to store and transmit tokens. To handle simple memory accesses, ReadMC_n is a n-port read-only memory controller, and WriteMC is a single-port write-only memory controller.

Firing rules in Fig. 4 should be considered as a formal dataflow specification for the concrete VHDL implementation provided in the Dynamatic tool. Implementing concretely those components in VHDL sometimes requires the addition of a state, either for performance or correctness reasons. For example, Fork is implemented in two variants: the lazy fork is stateless, closely following the specification in Figure 4, while the eager fork requires a state. Their behavior differ depending on the readiness of components connected to their outputs: the lazy fork only transmits to all of its successors when they are all ready, whereas the eager fork transmits to its successors as soon as they are ready, regardless of the status of the other successors. At the dataflow level, readiness isn't relevant: unbounded queues can always accept tokens. Other examples are Merge and CntrlMerge, implemented with an extra state to memorize, across several clock cycles, which token has been accepted. This is required in the VHDL implementation because their successor may not be able to receive that accepted token within the same clock cycle.

## 4 Circuits as Graphs with Cigr

This section presents Cigr, our graph-based IR for circuits. Circuits are graphs, where nodes are components and edges are channels. Such a graph-based IR is a natural encoding of a circuit, and easily integrable in a compilation pipeline. We start by defining the IR, then present its formal operational small-step semantics, and explain how to consider a circuit as a component itself. We
<figure><img src="image_6.png" /></figure>

A circuit made of two components *a* and *b*, with respective identifiers 0 and 1. Channels are represented as arrows labeled with channel identifiers: $\pi_1$ connects the first output port of *b* to the second input port of *a*, and $\pi_0$ connects the first output port of *a* to its first input port. Formally, the circuit is defined by the map $G = \{0 \mapsto (a, [\pi_0; \pi_1], [\pi_0; \pi_3]) ; 1 \mapsto (b, [\pi_2], [\pi_1])\}$. Assuming $a = (2, 2, \dots, \to_a \cdot)$ and $b = (1, 1, \dots, \to_b \cdot)$, the circuit graph is well-formed.

<caption>Fig. 5. Example of a simple circuit with two components</caption>

assume a set of components CMP, each of which can be referred to as an identifier from a set $Id_{CMP}$. We further assume a set of channel identifiers $Id_{CH}$.

## 4.1 Syntax of Cigr

*Definition 4.1 (Circuit graph).* A circuit graph is a finite map $G : Id_{CMP} \mapsto CMP \times Id_{CH} \times Id_{CH}$ from component identifiers to triples made of a component, the identifiers of the channels connected to the input ports and to the output ports of this component. We write $G[n]^c$ for the component associated to identifier $n$ in $G$ and we respectively write $G[n]^{in}$ and $G[n]^{out}$ for the channel identifiers connected to the input and output ports of $G[n]^c$ in $G$.

We emphasize that we distinguish ports of components from channels. Two components in a circuit are connected by associating a *common* channel identifier to their connected ports. Fig. 5 gives an example of a simple circuit.

For a circuit graph in Cigr to make sense, we introduce some structural constraints, leading to the notion of well-formedness. The example graph in Fig. 5 is well-formed.

*Definition 4.2 (Well-formed graph).* A circuit graph $G$ is well-formed, written $wf_{Cigr} G$, when it meets the three following conditions:

* Full-connectedness : $\forall n, |G[n]^{in}| = |G[n]^c|^{in} \wedge |G[n]^{out}| = |G[n]^c|^{out}$

* Unique input port of channels: $\forall n \, n' \, k \, k', G[n]^{in}[k] = G[n']^{in}[k'] \Rightarrow k = k' \wedge n = n'$

* Unique output port of channels: $\forall n \, n' \, k \, k', G[n]^{out}[k] = G[n']^{out}[k'] \Rightarrow k = k' \wedge n = n'$

Note that well-formedness does allow connecting a component with itself: connecting input ports and output ports of the same component does not violate the definition.

## 4.2 Small-Step Semantics of Cigr

The semantics of Cigr is defined as a stepping relation between circuit states. There are two parts in circuit state: the state of all components, and the state of all channels. A channel state describes the actual tokens waiting in it; we represent it as a simple list of tokens in $\vec{V}$.

*Definition 4.3 (Circuit state).* A circuit state is a pair $s = (s^{ch}, s^{cmp})$ where $s^{ch}$ is a finite map $Id_{CH} \mapsto \vec{V}$ from channel identifiers to unbounded queues of tokens, and $s^{cmp}$ is a finite map $Id_{CMP} \mapsto S$ from component identifiers to component states.

For the circuit of Fig. 5, the state $\{ (\pi_0 \mapsto [1]; \pi_1 \mapsto [4]; \pi_2 \mapsto [3]; \pi_3 \mapsto []), \{0 \mapsto \alpha; 1 \mapsto \beta\} \}$ describes that channel $\pi_3$ is empty, $\pi_2$ contains tokens 3 and 5 and that component 0 (resp. 1) is in state $\alpha$ (resp. $\beta$). Note that channel states only contain actual tokens from $\vec{V}$. This contrasts with other synchronous dataflow languages like Lustre [10], that would instead use optional tokens from $\vec{V}_2$ to signal the absence of a value, at precise clock timestamps. We, instead, are independent from any clock signal.
The semantic judgment of Cigr is written $G \Vdash s_1 \xrightarrow{(n,r)} s_2$ and describes, in a circuit G, the evolution of the circuit state from $s_1$ to $s_2$, when firing the component identified by $n$ with a rule labeled $r$. It is defined below in Definition 4.4. Starting with input tokens $\vec{i}$ taken from $s_1^{ch}$, it triggers firing rule $r$ of component $G[n]^c$, adds the produced tokens $\vec{o}$ to the resulting state $s_2^{ch}$ and updates the circuit's component state $s_1^{cmp}$ to $s_2^{cmp}$. This rule only makes sense for well-formed circuits. Indeed, $\{G[n]^{in} \mapsto \vec{i}\}$, denoting the pointwise map of identifiers in $G[n]^{in}$ to tokens in $\vec{i} \in \tilde{V}_2$, is well-defined only if $G[n]^{in}$ contains no duplicate channel identifiers.<fnref n="1" /> We write $s \cup s'$ for the pointwise concatenation of two maps of lists, where maps of lists default to the empty list: $\forall k, (s \cup s') [k] = s[k] \cdot s'[k]$.

**Definition 4.4 (Semantics of Cigr).**

$$ \frac{s_1^{ch} = \{G[n]^{in} \mapsto \vec{i}\} \cup s \quad (\vec{i}, s_1^{cmp}[n]) \xrightarrow{r} G[n]^c \quad (\vec{o}, \sigma) \\ s_2^{ch} = s \cup \{G[n]^{out} \mapsto \vec{o}\} \quad s_2^{cmp} = s_1^{cmp} [n \leftarrow \sigma] \\ \qquad G \Vdash s_1 \xrightarrow{(n,r)} s_2} $$

For the circuit G in Fig. 5 and the firing rule $([\langle 3 \rangle], \beta) \xrightarrow{r_0} ([\langle 7 \rangle], \beta')$, a possible step is:

$$ G \Vdash \begin{array}{l} (1, r_0) \\ \xrightarrow{\qquad} \left( \begin{array}{@{}l@{\quad}l@{}} \{ \pi_0 \mapsto [1]; & \pi_1 \mapsto [4]; \pi_2 \mapsto [3; 5]; \pi_3 \mapsto [] \}, & \{ 0 \mapsto \alpha; 1 \mapsto \beta \} \\ \{ \pi_0 \mapsto [1]; & \pi_1 \mapsto [4; 7]; \pi_2 \mapsto [5]; \pi_3 \mapsto [] \}, & \{ 0 \mapsto \alpha; 1 \mapsto \beta' \} \end{array} \right) \end{array} $$

In G, component b has identifier 1. When it fires rule $r_0$, token 3 is consumed from channel $\pi_2$ connected to its first (and only) input port, and a token value 7 is produced on its first (and only) output port, which is connected to channel $\pi_1$. Its state is updated from $\beta$ to $\beta'$.

As is standard, we write the reflexive-transitive closure of the stepping relation as $G \Vdash s_0 \xrightarrow{Cigr} \tilde{n}r \xrightarrow{*} s_m$, where $\tilde{n}r = [(n_1, r_1); (n_2, r_2); \dots; (n_m, r_m)] \in \mathrm{Id}_{\mathrm{CMP}} \times \mathcal{R}$ and $G \Vdash s_{i-1} \xrightarrow{Cigr} s_i$ for $i \in \{1, \dots, m\}$. This describes the execution of a circuit according to a schedule $\tilde{n}r$, where components successively execute in the order dictated by the schedule.

In the next section, we express semantic properties over *execution traces*, namely the history of all channels. The history of a channel is defined as the sequence of tokens that went through the channel, including those initially present (see Fig. 2c). For space reasons, we elide the formal definition of histories and traces, which we obtain by instrumenting the stepping relation of Cigr<fnref n="2" />.

**Definition 4.5 (Execution trace).** The trace of the execution $G \Vdash s \xrightarrow{Cigr} \tilde{n}r \xrightarrow{*} s'$ is a mapping in $\mathrm{Id}_{CH} \mapsto \tilde{V}$ from each channel identifier to its history.

Execution traces behave monotonically: extending an execution also extends the history of all channels, accordingly to the prefix relation. We write $\vec{a} \sqsubseteq \vec{b}$ when $\vec{a}$ is a prefix of sequence $\vec{b}$.

**LEMMA 4.6 (TRACE MONOTONICITY).** If execution $G \Vdash s \xrightarrow{Cigr} \tilde{n}r_1 \xrightarrow{*} s_1$ has trace $t_1$ and execution $G \Vdash s \xrightarrow{Cigr} \tilde{n}r_1 \xrightarrow{*} s_2$ has trace $t_2$, then $\forall \pi, t_1[\pi] \sqsubseteq t_2[\pi]$.

<footnote n="1">¹To lighten the notations, when required, we implicitly convert $\vec{i} \in \tilde{V}$ to a list in $\tilde{V}$ by converting $\langle x \rangle$ to $[x]$ and $\epsilon$ to $[\epsilon]$.</footnote>

<footnote n="2">²See the Coq development of our artifact [28] for full definitions.</footnote>
instrumentation only to express and prove properties; it doesn't alter the semantics of components or circuits. The judgment $G \models s \xrightarrow{Cigr} s'$ just traces the choice $u$ made when firing $G[n]^c$.

## 5.1 Functionality and Input-Determinism

The first two basic conditions on components capture the form of determinism we consider for components. First, components should be *functional*: when firing a rule, the produced output tokens and resulting component state are uniquely determined by the input tokens.

**Definition 5.1 (Functional component).** A component $c$ is functional whenever, for any two firing rules, $(\vec{i}, s) \xrightarrow{r,u} c(\vec{o}_1, s_1)$ and $(\vec{i}, s) \xrightarrow{r,u} c(\vec{o}_2, s_2)$, then $(\vec{o}_1, s_1) = (\vec{o}_2, s_2)$.

Second, components should be *input-deterministic*: when firing a given rule, they shouldn't have a choice on which subset of the input tokens to consume; only one subset should be allowed. Typically, $[\langle x \rangle; \epsilon]$ and $[\epsilon; \langle y \rangle]$ are both subsets of $[\langle x \rangle; \langle y \rangle]$, and being able to choose among them is possible only through different rule labels or different non-deterministic choices. For two input patterns $\vec{i}, \vec{i}' \in \mathcal{V}_2$, we write the input subset relation as $\vec{i} \le \vec{i}'$.

**Definition 5.2 (Input-deterministic component).** A component $c$ is input-deterministic whenever, for any two firing rules, $(\vec{i}_1, s) \xrightarrow{r,u} c(\vec{o}_1, s_1)$ and $(\vec{i}_2, s) \xrightarrow{r,u} c(\vec{o}_2, s_2)$, if $\vec{i}_1 \le \vec{i}$ and $\vec{i}_2 \le \vec{i}$, then $\vec{i}_1 = \vec{i}_2$.

We formulate both properties separately because they deal with different sources of non-determinism. Functionality disallows choices that are purely internal, while input-determinism disallows picking among several possible inputs. In the rest of the section, we assume components are satisfying both properties. In practice, this is easily achievable with a sensible instrumentation with rule labels and non-deterministic choices. Functionality and input-determinism lift from components to circuits graph components; we explain how we prove such a generalization in Section 6.3.

## 5.2 Parallelism

Parallelism is an inherent feature of concrete circuits: components should be able to execute in parallel, simultaneously. Unlike semantics such as Faustini's [21], that execute several components per semantic step, ours is by definition sequential: only one component executes per step. We made this design choice to favor simplicity in our operational model. Nevertheless, for a certain class of circuits, we prove that it satisfies a parallelism property: from a given state, the components that could execute can actually be executed in any order from this state, leading to the same state.

**Definition 5.3 (Parallelism).** A circuit $G$ is parallelizable when, for any state $s$ and for any subset of distinct fire rules $nr_1, \dots, nr_k \in \text{Id}_{\text{CMP}} \times \mathcal{R}$ that are firable in $s$ (i.e., for each $i$, there exists $s_i$ such that $G \models_{Cigr} s \xrightarrow{nr_i} s_i$), there exists $s'$ such that, for any permutation $\vec{n}\vec{r}'$ of $[nr_1; \dots; nr_k]$, $G \models_{Cigr} \vec{n}\vec{r}' \stackrel{*}{\to} s'$.

We prove that a circuit is parallelizable when all of its components satisfy a simpler yet similar property: any two firing rules with distinct labels can fire simultaneously, i.e., they can fire in any order (while making the same non-deterministic choice) and end on a same state. We call such components *confluent*. A circuit where all components have a singleton set for rule labels is always parallelizable, since such components are trivially confluent.

**Definition 5.4 (Confluent component).** A component $c$ is confluent if for any two firing rules $(\vec{i}_1, s) \xrightarrow{r_1, u_1} c(\vec{o}_1, s_1)$ and $(\vec{i}_2, s) \xrightarrow{r_2, u_2} c(\vec{o}_2, s_2)$ such that $r_1 \neq r_2$, then there is a state $s'$ such that $(\vec{i}_1, s_2) \xrightarrow{r_1, u_1} c(\vec{o}_1, s')$ and $(\vec{i}_2, s_1) \xrightarrow{r_2, u_2} c(\vec{o}_2, s')$.
**THEOREM 5.5.** Let $G$ be a circuit graph. If all its components are confluent, then $G$ is parallelizable.

**PROOF.** First, we prove that a circuit graph component made of confluent components is also confluent (see Section 6.3). Then, we prove that confluence implies Definition 5.3, by induction on $k$, the number of parallelizable firing rules. $\square$

## 5.3 Determinacy

Determinacy is specific to circuits implementing deterministic computations. Strictly speaking, our semantics is not deterministic: at each semantic step, any executable component may fire. Instead, we consider the notion of determinacy, as introduced by Karp and Miller [27]: all possible executions of a circuit results in the same computation, regardless of the scheduling of steps. In other words, the produced tokens must be uniquely determined by the tokens present in the initial state. In particular, different schedules must not result in different tokens being produced. Further, a token that is produced with one schedule and not with another schedule has, in fact, *not yet been produced*, and could be produced by extending this other schedule. Thus, we see two aspects in determinacy: the order in a given schedule should not matter, and tokens are produced in the same order regardless of the schedule.

We formalize the first aspect as follows: two schedules executing the same components in different orders correspond to the same computation, i.e., their final states and traces must be identical. This aspect goes beyond parallelizability: we must take into account *sequences* of executions, where the fired components could depend from each other.

**Definition 5.6 (Order irrelevance).** A circuit $G$ is order-irrelevant when, for any two executions $G \models_{\text{Cigr}} s \xrightarrow{\vec{n}_1}^* s_1$ and $G \models_{\text{Cigr}} s \xrightarrow{\vec{n}_2}^* s_2$ with respective traces $t_1$ and $t_2$, if schedules $\vec{n}_1$ and $\vec{n}_2$ are permutations of each other, then $s_1 = s_2$ and $t_1 = t_2$.

We formalize the second aspect as trace determinacy: for any two executions, and for each channel, if the history of this channel for one execution contains $k$ tokens and $k'$ for the other, such that $k \le k'$, then the first $k$ tokens of both histories must be equal. Equivalently, for each channel, histories must be prefixes of a same sequence of tokens. We then say that both traces are *flow equivalent*.

**Definition 5.7 (Flow equivalence).** Two execution traces $t_1, t_2 \in \text{Id}_{\text{CH}} \mapsto \vec{V}$ are flow equivalent, written $t_1 \rightsquigarrow t_2$, if for any channel $\pi$, there exists $\vec{x} \in \vec{V}$ such that $t_1[\pi] \subseteq \vec{x}$ and $t_2[\pi] \subseteq \vec{x}$.

**Definition 5.8 (Trace determinacy).** A circuit $G$ is trace-determinate when for any two executions $G \models_{\text{Cigr}} \vec{n}_1 \xrightarrow{\pi}^* s_1$ and $G \models_{\text{Cigr}} \vec{n}_2 \xrightarrow{\pi}^* s_2$, their respective traces $t_1$ and $t_2$ are flow equivalent: $t_1 \rightsquigarrow t_2$.

Not all circuits are order-irrelevant or trace-determinate, in particular because of non-deterministic components such as $\text{Merge}_2$. Yet, such components can still be used with due precaution in circuits to implement deterministic computations. It suffices to never *exercise* their non-determinism. To express such safe execution contexts, we first need to define, for a component $c$, a predicate $\text{safe}_c(\vec{i}, s)$ that indicates that $c$ behaves deterministically when presented with input tokens $\vec{i}$ in state $s$. A component equipped with such predicate is called a *safe component*.

**Definition 5.9 (Safe component).** The quadruple $c = (n_i, n_o, \rightarrow_c, \text{safe}_c)$ is a safe component if $(n_i, n_o, \rightarrow_c)$ is a confluent component and if $\text{safe}_c \in \vec{V}_? \times S$ meets the following conditions.

* Closure under input subset: $\forall \vec{i} \ \vec{i}', s, \text{safe}_c(\vec{i}, s) \wedge \vec{i}' \le \vec{i} \implies \text{safe}_c(\vec{i}', s)$.

* Safe determinism: $\forall \vec{i} \ s, \text{safe}_c(\vec{i}, s)$, then for any two firing rules $(\vec{i}_1, s) \xrightarrow{r, u_1}^{} c(\vec{o}_1, s_1)$ and $(\vec{i}_2, s) \xrightarrow{r, u_2}^{} c(\vec{o}_2, s_2)$ with $\vec{i}_1 \le \vec{i}$ and $\vec{i}_2 \le \vec{i}$, we have $u_1 = u_2$.
When safe<sub>c</sub>(ī, s) is true, we say that (ī, s) is a safe context for c.

For example, ([⟨x⟩; ε], ●) and ([ε; ⟨x⟩], ●) are two safe contexts for Merge<sub>2</sub>, whereas ([⟨x⟩; ⟨y⟩], ●) is not: Merge<sub>2</sub> could either consume ⟨x⟩ or ⟨y⟩. In our Coq development, we prove that Dynamic's components are safe. We formally define the predicate safe(·, ·) as follows, for both Merge<sub>n</sub> and CntrlMerge<sub>n</sub>. All other Dynamic's components are deterministic, and are thus safe in all contexts.

$$ \frac{|\vec{i}_{\epsilon}| = k \quad |\vec{i}_{\epsilon}'| = n - k - 1}{\text{safe}_{\text{Merge } n}(\vec{i}_{\epsilon} \cdot [\langle x \rangle] \cdot \vec{i}_{\epsilon}', \bullet)} $$

$$ \frac{|\vec{i}_{\epsilon}| = k \quad |\vec{i}_{\epsilon}'| = n - k - 1}{\text{safe}_{\text{CntrlMerge } n}(\vec{i}_{\epsilon} \cdot [\langle x \rangle] \cdot \vec{i}_{\epsilon}', \bullet)} $$

We extend safety to circuits: a circuit state is safe if all components are in safe contexts, and a circuit is safe from a state if all reachable states are safe.

**Definition 5.10 (Safety for circuits).** A state s is safe for circuit G, written safe<sub>G</sub>(s), whenever for all n, if G[n]<sup>in</sup> maps to ī in s<sup>ch</sup>, then for any input subset ī' ≤ ī, safe<sub>G[n]</sub>(ī', s<sup>cmp</sup>[n]). Moreover, a circuit G is safe from s, written safeFrom<sub>G</sub>(s), if: ∀n̄, s', G |= s s̄ →<sup>*</sup> s' =⇒ safe<sub>G</sub>(s').

We are now able to state and prove that circuits are determinate for safe states.

**THEOREM 5.11 (DETERMINACY OF SAFE CIRCUITS).** Let G be a circuit and s a state. If safeFrom<sub>G</sub>(s), then G is order-irrelevant and trace-determinate, for executions starting from s.

**PROOF.** Again, we proceed in two steps. We first lift safe determinism from components to circuits (see Section 6.3). We then prove the actual properties. We prove order irrelevance by induction on the length of schedules. To prove trace determinacy, we rely on Lemma 5.12 below about trace confluence, and conclude with the monotonicity of traces (Lemma 4.6). □

**LEMMA 5.12 (TRACE CONFLUENCE).** Let G be a circuit graph all of whose components are confluent. Suppose G |= s s̄ →<sup>*</sup> s<sub>1</sub> with trace t<sub>1</sub> and G |= s s̄ →<sup>*</sup> s<sub>2</sub> with trace t<sub>2</sub>. Then, then there exists s', two schedules n̄'<sub>1</sub> and n̄'<sub>2</sub> and traces t'<sub>1</sub> and t'<sub>2</sub> such that G |= s<sub>1</sub> s̄ →<sup>*</sup> s' with trace t<sub>1</sub> ∪ t'<sub>1</sub>, and G |= s<sub>2</sub> s̄ →<sup>*</sup> s' with trace t<sub>2</sub> ∪ t'<sub>2</sub>, and t<sub>1</sub> ∪ t'<sub>1</sub> = t<sub>2</sub> ∪ t'<sub>2</sub>.

Determinacy holds for executions that only go through safe states. We emphasize that circuits with only deterministic components are trivially safe from any well-formed state. For circuits with non-deterministic components, the safety of specific states needs to be proved on a case-by-case basis, for each circuit. A possible strategy to prove this is to enclose non-deterministic components in subcircuits that ensure deterministic behaviors, like the *well-formed merge structures* introduced by Woo [43] for non-deterministic merges. We give an example in Fig. 6, where we proved that the circuit is safe from states in which there is at most one token among all internal channels. Proving this kind of invariant in Cigr is not too difficult, because we know the *exact structure* of the circuit: we know which channels are internal channels and the components they are connected to.

So far, we have kept deferring the generalization of property from components to circuits. Indeed, even though Cigr is fine for proofs on specific circuits, its simple definition does not help proving meta-properties about classes of circuit, where all kinds of wiring are possible. Ideally, one would employ an inductive proof methodology, which lacks in Cigr. In the next section, we present Cilan, our second IR for circuits, where circuits and their semantics are defined inductively.
<figure><img src="image_7.png" /></figure>

This circuit propagates the inputs x either to f or g, which are both stateless, depending on the value of the inputs c, then transmits the result to the output r. The Gate component transmits a token from c to Branch only when it receives a token from the fork. The Fork-Gate path ensures that no token is transmitted to f or g, as long as one of them has an on-going computation. Therefore, this circuit is safe from states in which there is at most one token among all internal channels.

<figure><img src="image_8.png" /><figcaption>Fig. 7. Cilan</figcaption></figure>

# 6 Circuits as Terms with Cilan

Cilan is a core term calculus in which circuits are composed inductively through dedicated constructs. Thanks to its inductive nature, Cilan facilitates formal reasoning: it allows for inductive proofs of meta-properties of the semantics of circuits. In particular, we show how we prove, using Cilan, that properties stated on components lift to circuits. Thanks to the semantic equivalence between Cilan and Cigr (see Section 7), properties proven on Cilan also hold on Cigr.

## 6.1 Syntax of Cilan

The syntax of Cilan is given in Fig. 7a. The base case for circuits terms is a single component unit {$n \mapsto (c, \vec{\pi}_i, \vec{\pi}_o)$}, which associates identifier $n \in \text{Id}_{\text{CMP}}$ to component $c \in \text{CMP}$, and channel identifiers $\vec{\pi}_i$ and $\vec{\pi}_o$ to respectively input and output ports of c. This corresponds to a singleton map in Cigr. The parallel composition $T \star T'$ of circuits T and T' juxtaposes them, leaving their wiring untouched. The self-composition $\uparrow T$ is where the wiring happens. It wires the first output port of circuit T to its first input port. When convenient, we use the notation $\uparrow_{\pi'}^T T$, to indicate that $\pi'$ (resp. $\pi$) is the channel identifier at the first input (resp. output) of T. After the self-composition, though, both channels should be considered as identifying a same and unique channel $\pi'$. Wiring between arbitrary input and output ports is made possible with the remapping construct $\chi_{\omega_o}^{\omega_i} T$, that applies a permutation $\omega_i$ (resp. $\omega_o$) to the inputs (resp. output) ports of T. We write permutations as tuples of ports numbers, in the set $W_k$.

Figure 8 illustrates Cilan's syntax on the previous Cigr example from Fig. 5. The two component units are $T_a$ and $T_b$. Component $T_a$ is first self-composed to merge channels $\pi_4$ to $\pi_0$. It is then composed in parallel with $T_b$. Next, the positions of the outputs $\pi_3$ and $\pi_5$ are swapped, using the permutation $(2, 1)$. Input channels are not touched by the remapping, so we use the identity permutation $(1, 2)$. Finally, another self-composition merges channels $\pi_5$ to $\pi_1$. In Cilan, several
$$ \begin{array}{c} \uparrow_{\pi_5}^{\pi_1} \times_{(2,1)}^{(1,2)} ((\uparrow_{\pi_4}^{\pi_0} T_a) \star T_b) \\ \text{with } \left\{ \begin{array}{l} T_a = \{0 \mapsto (a, [\pi_0; \pi_1], [\pi_4; \pi_3])\} \\ T_b = \{1 \mapsto (b, [\pi_2], [\pi_5])\} \end{array} \right. \end{array} $$

<figure><img src="image_9.png" /><figcaption>Fig. 8. Example circuit in Cilan: the term on the left is graphically represented on the right. Subterms are enclosed in dashed boxes, and channels connect subterms. Self-compositions shadows the output channel identifier of their subterms, here written in parentheses.</figcaption></figure>

terms may represent, morally, the same circuit. For instance, reordering two parallel compositions would represent the same circuit.

While in Cigr, identifiers of both components and channels are directly available from the circuit map, the syntax of Cilan requires defining these sets inductively. We elide their definitions for brevity. For a circuit term $T$, we write $T^{cs}$ for the set of all component identifiers occurring in $T$. Defining the channels of $T$ requires more care, due to how self-composition expresses wiring. Similarly to Cigr, we define $T^{in}$, $T^{out}$ and $T^{\uparrow}$ for the input, output and internal channels of $T$, respectively. By convention, the sole identifier of the internal channel of $\uparrow_{\pi}^{\pi'} T$ is $\pi'$, at the input port of $T$, and $\pi$ is not considered to be a channel of the self-composition at all. So, even though both $\pi$ and $\pi'$ are channels of $T$, $\pi'$ is an internal channel of $\uparrow_{\pi}^{\pi'} T$, but $\pi$ is not a channel of $\uparrow_{\pi}^{\pi'} T$. The set $T^{\Pi s}$ of all channel identifiers of $T$ is then the disjoint union of $T^{in}$, $T^{out}$ and $T^{\uparrow}$.

As for Cigr, we only consider terms that are well-formed, according to the following conditions. A component unit $\{n \mapsto (c, \vec{\pi}_i, \vec{\pi}_o)\}$ is well-formed when $\vec{\pi}_i$ and $\vec{\pi}_o$ specify channel identifiers for each and every port of component $c$ and all identifiers within $\vec{\pi}_i \cdot \vec{\pi}_o$ are distinct. Term $T \star T'$ is well-formed when $T$ and $T'$ are well-formed and separated: there must be no conflict in component identifiers nor channel identifiers. Self composition $\uparrow T$ is well-formed when $T$ is well-formed. Finally, $\chi_{\omega_o}^{\omega_i} T$ is well-formed when $\omega_i$ and $\omega_o$ are permutations, respectively in $W_{|T^{in}|}$ and $W_{|T^{out}|}$.

**Definition 6.1 (Well-formed Cilan terms).** The well-formedness of a term $T$, written as predicate $wf_{Cilan} T$, is defined inductively on the structure of $T$ as follows.

$$ \frac{ |\vec{\pi}_i| = |c|^{in} \qquad |\vec{\pi}_o| = |c|^{out} \qquad T^{cs} \cap T'^{cs} = \emptyset \qquad T^{\Pi s} \cap T'^{\Pi s} = \emptyset \qquad \begin{array}{l} \text{wf}_{\text{Cilan}} T \\ \text{wf}_{\text{Cilan}} T' \end{array} \qquad \begin{array}{l} \text{wf}_{\text{Cilan}} T \\ \text{wf}_{\text{Cilan}} (\uparrow T) \end{array} \qquad \begin{array}{l} \omega_i \in W_{|T^{in}|} \\ \omega_o \in W_{|T^{out}|} \\ \text{wf}_{\text{Cilan}} T \\ \text{wf}_{\text{Cilan}} (\chi_{\omega_o}^{\omega_i} T) \end{array} }{ \text{wf}_{\text{Cilan}} (\{n \mapsto (c, \vec{\pi}_i, \vec{\pi}_o)\}) } \qquad \text{wf}_{\text{Cilan}} (T \star T') $$

**Remark 6.2.** The example term in Fig. 8 is well-formed, in particular because all channels identifiers that are syntactically present in the term are unique. However, this is not a necessary condition: a channel identifier may appear multiple times in the syntax of a well-formed term as long as only one occurrence of this identifier subsists after removing output channel identifiers of self-compositions. For example, if we substitute $T_b$ in Fig. 8 with $T'_b = \{1 \mapsto (b, [\pi_2], [\pi_4])\}$ (this is $T_b$ where we replaced $\pi_5$ with $\pi_4$), we obtain the term $\uparrow_{\pi_4}^{\pi_1} \times_{(2,1)}^{(1,2)} ((\uparrow_{\pi_4}^{\pi_0} T_a) \star T'_b)$ which is well-formed despite $\pi_4$ appearing syntactically multiple times. This is because $\pi_4$ is no longer a channel identifier of $\uparrow_{\pi_4}^{\pi_0} T_a$.
## 6.2 Small-Step Semantics of Cilan

As for Cigr, we define the semantics of Cilan in a small-step, operational style, labeling each step with the identifier of the component that fires a given rule label. To define the semantic stepping rule, however, we exploit the inductive nature of Cilan, which enables a built-in compositionality in the syntax of circuits. In particular, we are able to define how a component fires in a circuit by induction on the structure of the term. This amounts to defining firing rules for circuit terms, of the form $(\vec{i}, s) \xrightarrow{(n,r)}_T (\vec{o}, s')$, meaning that $T$ fires component $n$ with rule $r$, following the input and output patterns $\vec{i}$ and $\vec{o}$, updating the internal state of the term from $s$ to $s'$.

Internal states for Cilan terms aren't simple, flat mappings from channel identifiers to token queues, and from component identifiers to component states. Instead, an internal state mimicks the structure of term, and associates, by induction on the structure of the term, channel identifiers to token queues and component identifiers to component states. The internal states of terms are defined in Fig. 7b. For a component unit, it is the state of its underlying component. The internal state of a parallel composition is written $s_1 \star s_2$, and separates the respective states of subterms. The internal state of a self-composed circuit $\uparrow_{\pi'}^{\pi'} T$ is written $\uparrow_{\vec{l}}^s T$, where $s$ is the internal state of $T$, and $\vec{l}$ is the token queue of the connection established between channels $\pi$ and $\pi'$, i.e., the internal channel created with the self-composition. Finally, the internal state of a remapped circuit $\chi_{\omega_o}^{\omega_i} T$ is simply the one of $T$: remapping inputs and outputs in a term does not affect its internal state.

Firing rules for terms are defined in Fig. 9. There, we use the following notations. We write $\vec{a} \odot \vec{b}$ for the concatenation of $\vec{a}$ and $\vec{b}$. To lighten the notations, when used on lists in $\vec{A}_2$, the list concatenation coerces $\langle a \rangle$ to $[a]$ and $\epsilon$ to $[]$ depending on the context. Rule FIRECMP simply fires, in a component unit term, the designated rule of the component. In rules for parallel compositions, FIREPCOMPL and FIREPCOMP R, only the subterm containing component $n$ fires; the other subterm is idle, thereby consuming and producing no token at all. To fire $(n, r)$ in a self-composed circuit, in rule FIRESCOMP, we fire the underlying “disconnected” subterm, i.e., without the connection from the first output to the first input. It modifies the internal term state, potentially consuming an optional token $v$ and producing an optional token $v'$ in the queue of the connecting channel. Lastly, rule FIREREMAP fires the subterm and applies the permutations $\omega_i$ and $\omega_o$ on the consumed inputs and produced outputs.

We are now ready to define the Cilan stepping relation for circuits. To describe the state of the whole circuit, in addition to the internal state of the term, we also need to keep track of the token queues for input and output channels of the term, i.e., those channels which are not internal, and connected either to only input ports, or output ports. A circuit state $\sigma$ is thus a triple $(\vec{i}, \vec{o}, s)$ where $\vec{i}, \vec{o} \in \vec{V}$ are the token queues for input and output channels in $T^{\text{in}}$ and $T^{\text{out}}$, and where $s$ is the internal state of $T$. The semantic judgment for Cilan is written $T \models_{\text{Cilan}} \sigma \longrightarrow^{(n,r)} \sigma'$. It is defined as firing the rule $(n, r)$ in term $T$, updating the circuit state from $\sigma$ to $\sigma'$.

$$ \frac{\substack{\text{STEPCILAN} \\ \vec{i} = \vec{i}'' \odot \vec{i}'}}{T \models_{\text{Cilan}} (\vec{i}, \vec{o}, s) \longrightarrow^{(n,r)} (\vec{i}', \vec{o}', s')} $$

where $\vec{a} \odot \vec{b}$ denotes the pointwise concatenation of lists of lists, with $\vec{a}$ and $\vec{b}$ of equal length.

In the following, we assume that states structurally match their associated terms, e.g. the state of $\uparrow T$ must be of the form $\uparrow_{\vec{l}}^s T$, where $s$ recursively matches $T$.
<figure><img src="image_10.png" /><figcaption>Fig. 9. Firing rules for Cilan terms</figcaption></figure>

*Definition 6.3 (Well-formed state)*. A state $(\vec{i}, \vec{o}, s)$ is well-formed for a term $T$ when $|\vec{i}| = |T^{\text{in}}|$, $|\vec{o}| = |T^{\text{out}}|$, and the internal state $s$ structurally matches $T$.

## 6.3 Inductive Proofs with Cilan

In Section 5, we lifted properties of components to circuits, going through the construction of a circuit graph component. Instead of doing this proof on Cigr, we use Cilan to benefit from its inductive nature. We then transfer these properties back to Cigr by using the semantic equivalence proved in Section 7. Similarly to Section 5, we instrument the semantics of Cilan to make non-deterministic choices explicit, and label rules with $(n, r, u)$ where $u$ is the non-deterministic choice. As an example, let us prove the confluence property.

**THEOREM 6.4.** If all components of a term $T$ are confluent, then $T$ is also confluent: if we have $(\vec{i}_1, s) \xrightarrow{n_1, r_1, u_1} T (\vec{o}_1, s_1)$ and $(\vec{i}_2, s) \xrightarrow{n_2, r_2, u_2} T (\vec{o}_2, s_2)$ such that $(n_1, r_1) \neq (n_2, r_2)$, then there exists a state $s'$ such that $(\vec{i}_1, s_2) \xrightarrow{n_1, r_1, u_1} T (\vec{o}_1, s')$ and $(\vec{i}_2, s_1) \xrightarrow{n_2, r_2, u_2} T (\vec{o}_2, s')$.

**PROOF.** We proceed by induction on $T$. Each case focuses on different but precise aspects of $T$. The first case is the base case (single component) and is immediate by the hypothesis that all components are confluent. The case of $\chi_{\omega_o}^{\omega_i} T$ focuses on the impact of reordering the interface of $T$; for this property, its impact is essentially administrative, as the internal state is untouched. The case of $T_1 \star T_2$ focuses on the evolution of two independent subterms, that share no component and no channel. Two sub-cases are possible: either only one subterm makes both steps and the other one stays idle, or both subterms make one step. The independence of both subterms makes this case simple to conclude. The most interesting case is the self-composition $\uparrow_{\pi}^{\pi'} T$, which updates the single internal connecting channel $\pi'$. We prove this case by relying on the well-formedness of the term: each input port is associated to at most one rule label of one component, and the same goes for output ports. Because $(n_1, r_1) \neq (n_2, r_2)$, at most one step consumes a token in $\pi'$, and at most one produces a token in it. We then conclude quite straightforwardly by analyzing all cases. $\square$

## 7 Semantic Equivalence between Cigr and Cilan

We now prove that Cigr and Cilan are semantically equivalent. We first describe how to translate a term to a graph and vice versa, focusing on the important properties of the translations, rather than
on their concrete implementations. Our semantic equivalence theorem primarily serves transferring
meta-properties between both IR, so there would be little use in crafting optimized translation
algorithms. We then present our semantic equivalence theorem.

## 7.1 Syntactical Correspondence

We first define a predicate, $T \rightsquigarrow G$, to specify the syntactical matching between a circuit term $T$ and a circuit graph $G$. Intuitively, a term $T$ syntactically matches a graph $G$ when they have the same components and same connections: for any component identifier $n$, the component identified by $n$ must be the same in $T$ and in $G$, and its interface must be the same in $T$ and in $G$ (i.e., the input and output channel identifiers connected to the component must be the same). As a specification for our translations, this predicate specifies, with respect to $T$, the three mappings defining $G$, namely $G[\cdot]^c$, $G[\cdot]^in$[·] and $G[\cdot]^{out}[\cdot]$. Consequently, we define the following three predicates, inductively on $T$: predicate $T \rightsquigarrow^n c$ $c$ denotes that component $c$ is identified by $n$ in $T$, predicate $T \rightsquigarrow^{n} \pi$ denotes that $\pi$ are the identifiers of the channels connected to the input ports of $n$, and predicate $T \rightsquigarrow^{n,k}_{out} \pi$ denotes that $\pi$ is the identifier of the channel connected to the $k$-th output port of $n$.

*Definition 7.1 (Syntactic matching)* $\cdot \rightsquigarrow \cdot$). Let $T \in$ Cilan and $G \in$ Cigr. Suppose that $wf_{Cilan} T$. We say that $T$ and $G$ are syntactically matching, written $T \rightsquigarrow G$, whenever three conditions hold:

$$ \forall n, T \rightsquigarrow^n_c G[n]^c \quad \forall n, T \rightsquigarrow^{n}_{in} G[n]^{in} \quad \forall n k, T \rightsquigarrow^{n,k}_{out} G[n]^{out}[k] $$

For space reasons, we omit here their formal definitions (given in Appendix A). Predicates $\cdot \rightsquigarrow_c \cdot$ and $\cdot \rightsquigarrow_{in} \cdot$ are straightforward: we traverse the term to associate the component identifier with the right component or input channel identifiers. Predicate $\cdot \rightsquigarrow_{out}^{\cdot, \cdot}$ is defined similarly to $\cdot \rightsquigarrow_{in} \cdot$, except for the self-composition, which renames output channels. For a term $\uparrow_{\pi_1}^{\pi_2} T$, channel $\pi_2$ is the $k$-th output channel of component identified by $n$ in $\uparrow_{\pi_1}^{\pi_2} T$ only if $\pi_1$ is the $k$-th output channel of $n$ in $T$. Otherwise, $\pi$ is connected to the same output port of the same component in both the self-composed term and the bare term. Formally:

$$ \frac{T \rightsquigarrow^{n,k}_{out} \pi_1}{(\uparrow_{\pi_1}^{\pi_2} T) \rightsquigarrow^{n,k}_{out} \pi_2} \qquad \frac{T \rightsquigarrow^{n,k}_{out} \pi}{(\uparrow_{\pi_1}^{\pi_2} T) \rightsquigarrow^{n,k}_{out} \pi} \quad \pi \neq \pi_1 $$

Both predicates $\cdot \rightsquigarrow_c \cdot$ and $\cdot \rightsquigarrow_{out}^{\cdot, \cdot}$ are not affected by the remapping operator $\chi_{\omega_o}^{\omega_i} T$ because this operator only modifies the interface of the term and does not change the interface of components.

Translating a term $T$ in Cilan to $G$ in Cigr is done with a translation function toCigr, and is relatively straightforward. We first extract from the term each of the three mappings for components, input channel identifiers, and output identifiers, by recursively traversing $T$. We then aggregate in a triple, for each component identifier, the component itself and the channel identifiers, to build the resulting map $G$. Essentially, toCigr closely follows the ideas of the matching predicate between a term and a graph. We prove that toCigr, operating on well-formed terms, produces a matching, well-formed graph.

**LEMMA 7.2 (toCigr YIELDS A MATCHING WELL-FORMED GRAPH).** Let $T \in$ Cilan, such that $wf_{Cilan} T$. Then $T \rightsquigarrow$ toCigr($T$) and $wf_{Cigr}$ toCigr($T$).

Translating a well-formed circuit graph in Cigr to a term in Cilan is more involved: we need to recover a structured term from the graph mapping. We take inspiration from the normalization of network algebra described in [41]. The general idea, that we illustrate Fig. 10, is as follows. First, we entirely disconnect the circuit graph by introducing fresh identifiers for output channels connecting
<figure><img src="image_11.png" /><figcaption>Fig. 10. Translation of an example graph to a circuit term.</figcaption></figure>

components. We also keep track of the renaming applied when introducing these fresh identifiers. Second, we assemble all components using as many parallel compositions as needed. This leads to a well-formed term, but in which there is no wiring yet. Third, we connect components of this term, using as many self-compositions and remappings as needed. This wiring step in the translation uses the renaming information we gathered in the first step.

This translation process is done with the function toCilan. It is significantly harder to specify (see Appendix B): we must express all the right constraints related to the renaming phases for disconnecting the graph and reconnecting the term with the inverse renaming. We then prove that toCilan produces a well-formed, syntactically matching term.

LEMMA 7.3 (toCilan YIELDS A SYNTACTICALLY MATCHING WELL-FORMED TERM). Let $G \in \text{Cigr}$, such that $\text{wf}_{\text{Cigr}} G$. Then toCilan($G$) $\rightsquigarrow$ $G$ and $\text{wf}_{\text{Cilan}}$ toCilan($G$).

## 7.2 Semantic Equivalence

We prove the semantic equivalence between a graph and a term that are syntactically matching. Our theorem below lets us convert semantic steps back and forth between both semantics. It takes the form of a typical compiler correctness result about the translations toCigr and toCilan.

We first define an equivalence on states, as a three-place relation $\sigma \sim_T s$, between a term state $\sigma$ and a channel map $s$, relatively to the channel identifiers of $T$. This relation only holds on term states $\sigma$ that are well-formed for $T$ (Definition 6.3), and when $T$ is itself well-formed. Indeed, in a well-formed term $T$, channel identifiers are unique$^3$, which ensures that the matching map $s$ is well-defined. Relation $\sigma \sim_T s$ is morally simple: it essentially bridges the structural gap between $\sigma$ and $s$, the effective contents of channels is then required to be the same.

*Definition 7.4 (State matching* $\cdot$ *\dotfill*)*. Let $T \in \text{Cilan}$, such that $\text{wf}_{\text{Cilan}} T$. Let $\sigma$ be a well-formed term state for $T$, and let $s$ be a graph state. We say that states $\sigma$ and $s$ match with respect to $T$, written $\sigma \sim_T s$, when for any channel identifier $\pi$ of $T$, the value associated to $\pi$ in $\sigma$ is $s^{\text{ch}}[\pi]$, and when for all component identifier $n$ of $T$, the value associated to $n$ in $\sigma$ is $s^{\text{cmp}}[n]$.

Our formal semantic equivalence theorem is as follows.

THEOREM 7.5 (SEMANTIC EQUIVALENCE BETWEEN Cigr AND Cilan). Let $G \in \text{Cigr}$, $T \in \text{Cilan}$ be such that $\text{wf}_{\text{Cigr}} G$, $\text{wf}_{\text{Cilan}} T$ and $T \rightsquigarrow G$. Let $s$ and $\sigma$ be such that $\sigma \sim_T s$. For all $n$ and $r$, we have

$$ 
\begin{array}{lclcl}
\forall s', G & \stackrel{\text{Cigr}}{\models} & s & \stackrel{n,r}{\longrightarrow} & s' \\
\forall s', T & \stackrel{\text{Cilan}}{\models} & \sigma & \stackrel{n,r}{\longrightarrow} & \sigma' \\
& & \exists s', T & \stackrel{\text{Cilan}}{\models} & \sigma \stackrel{n,r}{\longrightarrow} \sigma' \wedge \sigma' \sim_T s' \\
& & \exists s', G & \stackrel{\text{Cigr}}{\models} & s \stackrel{n,r}{\longrightarrow} s' \wedge \sigma' \sim_T s'
\end{array}
$$

<footnote>$^3$Well-formedness doesn't forbid syntactic duplicates of channel identifiers in the term. But, recall that the output channel identifier of a self-composed subterm of $T$ is no longer a channel identifier of $T$. See Remark 6.2</footnote>
We use this theorem to transfer properties proven on Cilan back to Cigr. As an example, let us transfer the confluence property (Theorem 6.4) to Cigr. Let $G \in \text{Cigr}$ be a well-formed graph and two steps whose firing rules are identified by $(n_1, r_1)$ and $(n_2, r_2)$ such that $(n_1, r_1) \neq (n_2, r_2)$. We know that $\text{toCilan}(G) \rightsquigarrow G$ (Lemma 7.3). By using the first implication of Theorem 7.5, we replicate these two steps on $\text{toCilan}(G)$. Theorem 6.4 introduces two new steps, that we replicate on $G$ using the second implication of Theorem 7.5. We conclude by proving that these two new steps end on the same state.

# 8 Experimental Validation

We empirically validate our semantics for dataflow circuits against Dynamatic's by executing our own interpreter of Cigr circuits. This section presents our interpreter and our experiment setup.

## 8.1 Interpreter

Our interpreter is parameterized by an interpreter of components. Given a set of components CMP, an interpreter of components is a function $\text{CMP} \to \mathcal{R} \to \vec{V}_\beta \to \mathcal{S} \to (\vec{V}_\beta \times \vec{V}_\beta \times \mathcal{S})_\beta$ that represents the firing relations. It takes a component, a rule label, a list of optional input tokens and a state, and it either returns $\epsilon$ if no firing rule is applicable, or a triple $\langle (\vec{i}', \vec{o}, s') \rangle$ where $\vec{i}'$ contains the input tokens that were consumed by the firing rule, $\vec{o}$ contains the output of the firing rule and $s'$ is the next state. The interpreter is correct if it behaves accordingly to the firing relation of CMP.

*Definition 8.1 (Component interpreter correctness).* An interpreter called $\text{ interp\_cmp}$ of a set of components CMP is correct if for all $c \in \text{CMP}, r \in \mathcal{R}, \vec{i} \in \vec{V}_\beta$ and $s \in \mathcal{S}$, we have:

$$ \text{ interp\_cmp}(c, r, \vec{i}, s) = \langle (\vec{i}', \vec{o}, s') \rangle \implies \vec{i}' \le \vec{i} \wedge (\vec{i}', s) \xrightarrow{r} c (\vec{o}, s') $$

Given a component interpreter $\text{ interp\_cmp}$, the interpreter of circuits $\text{ interp\_step}$ is a partial function that takes a circuit, a component identifier, a rule label and a state as input and returns the updated state if it is able to execute the provided component. We prove that our interpreter is correct with regards to Cigr semantics, provided that $\text{ interp\_cmp}$ is correct.

**THEOREM 8.2 (INTERPRETER CORRECTNESS).** Any interpreter step is an execution step in Cigr: $\forall G n r s s', \text{ interp\_step}(G, n, r, s) = \langle s' \rangle \implies G \models s \xrightarrow{n,r} s'$.

Consequently, properties presented in Section 5 also hold for the interpreter. In particular, when working on safe states, the interpreter is determinate. Therefore, all schedules of the interpreter correspond to the same computation. We run our interpreter using a round-robin scheduler that executes components one after another; this scheduler is simple and avoids starvation: all components are regularly scheduled to execute.

## 8.2 Experimental Setup

The goal of our experiment is to test our semantics against Dynamatic. We use Dynamatic to generate a circuit and its trace. We then convert this circuit into a Cigr circuit, run the interpreter to generate another trace. We finally compare both traces using a validator. More precisely, our setup is illustrated in Fig. 11. We first use Dynamatic to compile a C function into a dataflow circuit (DC). Then, we use it again to compile the dataflow circuit to VHDL and to generate a testbench. We simulate it using ModelSim [34] to generate a trace. This trace consists of the state of each channel (i.e., its data and control values) at each clock cycle. Simulating a circuit requires a testbench, whose role is to create a testing environment where the circuit is run, configure its initial state and provide it with input data. Here, the testbenches are generated by Dynamatic. Their input data and expected
<figure><img src="image_12.png" /><figcaption>Fig. 11. Experimental validation setup</figcaption></figure>

<table><caption>Table 1. Size of our code base in lines of code of Coq (left) and OCaml (right).</caption><thead><tr><th></th><th>Spec</th><th>Proofs</th><th></th><th>Code</th></tr></thead><tbody><tr><td>IR + Properties</td><td>4164</td><td>5015</td><td>Extracted Coq</td><td>2897</td></tr><tr><td>Interpreter</td><td>475</td><td>399</td><td>Driver</td><td>776</td></tr><tr><td>Utilities</td><td>3203</td><td>4260</td><td></td><td></td></tr><tr><td>Dynamatic</td><td>1454</td><td>894</td><td></td><td></td></tr></tbody></table>

outputs are derived from the C code: each kernel is defined alongside a main function that calls the kernel and that is processed by Dynamatic when generating testbenches.

We then convert the dataflow circuit into a Cigr circuit, and the raw trace into a Cigr trace with a custom-made parser. The circuit conversion consists in attributing identifiers to components and channels, and removing unrequired data such as timing data. The trace conversion abstracts away the control signals of the communication protocol used between components. The resulting trace only keeps the token transactions, i.e., the histories of all channels.

Then, we run our interpreter (extracted from our Coq development into OCaml) in order to generate the circuit trace. The interpreter is run by a driver that we wrote: it loads a circuit and configures its initial state and input data. In essence, our driver is akin to a testbench generator and a simulation engine. Dynamatic's circuits are initially empty and contain no token. They are given their input tokens during the initialization of the simulation. We replicate this on our end by starting our interpreter on similar states where all channels are empty, save for the input channels that we fill by using Dynamatic's trace. Finally, we compare Dynamatic's trace and our trace with a validator (extracted from our development) that verifies the flow equivalence of both traces.

We give the size of our Coq development and the extracted OCaml interpreter in Table 1. We recall that our development is parameterized by a set of components. Hence, the Dynamatic row corresponds to the instantiation of our work with Dynamatic's components, which consists in defining their firing rules and proving their safety, as defined in Section 5.3.

## 8.3 Tested Circuits, Results

Our semantics handles kernels that perform operations on scalar data, branches and loops, and perform simple memory accesses through read-only memories and single-writer memories. We tested our semantics on programs from Dynamatic's test suite that fit these characteristics. This corresponds to 11 programs for numeric computations (e.g. GCD), algorithms (e.g. binary search)
<table><caption>Table 2. Tested programs and their number of components, channels, read-only and single-writer memories.</caption><thead><tr><th>Kernel Name</th><th>Components</th><th>Channels</th><th>Reader</th><th>Writer</th></tr></thead><tbody><tr><td>binary_search</td><td>169</td><td>253</td><td>2</td><td>0</td></tr><tr><td>gcd</td><td>218</td><td>305</td><td>0</td><td>0</td></tr><tr><td>fir</td><td>48</td><td>63</td><td>2</td><td>0</td></tr><tr><td>if_loop_1</td><td>57</td><td>76</td><td>1</td><td>0</td></tr><tr><td>if_loop_2</td><td>51</td><td>69</td><td>1</td><td>0</td></tr><tr><td>if_loop_3</td><td>73</td><td>104</td><td>2</td><td>0</td></tr><tr><td>matrix</td><td>132</td><td>176</td><td>2</td><td>1</td></tr><tr><td>matvec</td><td>89</td><td>119</td><td>2</td><td>1</td></tr><tr><td>sobel</td><td>349</td><td>505</td><td>3</td><td>1</td></tr><tr><td>stencil_2d</td><td>140</td><td>187</td><td>2</td><td>1</td></tr><tr><td>sumi3_mem</td><td>42</td><td>56</td><td>1</td><td>0</td></tr></tbody></table>

**Listing 1** Source file matvec.c. The generated circuit is made of 89 components and 119 channels.

```c
int matvec(int m[N][N], int v[N], int out[N]) {
    int tmp = 0;
    for (int i = 0; i < N; i++) {
        tmp = 0;
        for (int j = 0; j < N; j++)
            tmp += v[j] * m[i][j];
        out[i] = tmp;
    }
    return tmp;
}
```

and matrix computations (e.g. multiplication, convolution). These are listed in Table 2. We give an example of such a kernel in Listing 1.

On all test programs, we make the reasonable assumption that circuits generated by Dynamatic avoid unsafe states, and are thus trace determinate. Indeed, because determinism is an important property that Dynamatic aims to attain, extra control logic is added to circuits to ensure that non-deterministic components always behave deterministically [25]. In practice, in Dynamatic, the only cause of potentially unsafe states are non-deterministic merge components. Consequently, we know that traces of all executions are flow equivalent, and it is sufficient to use a single run of the circuit to extract the reference trace generated by both Dynamatic and our interpreter.

On all examples, the trace of our interpreter is flow equivalent to Dynamatic's trace, the return values are the same, and all memory controllers (generated from arrays in the original programs, like m, v and out in Listing 1) end up in the same state. This demonstrates that our formal semantics for dataflow circuits is faithful to the Dynamatic HSL tool.

## 9 Related Work

Throughout the paper, we already discussed a number of previous works on the general topic of dataflow models, as well as some precise sources of inspiration we used in our formalization. We discuss below some of our technical choices, as well as broader considerations related to our formalization work.
As already discussed in Section 5.2, our semantics is defined in a sequential manner: one component fires at each computation step. Instead of having built-in parallelism, we prove a parallelism property for our semantics. Faustini [21] takes a different approach: several components can fire at each semantic step. But in turns, one must express some conditions on semantic states in order to avoid conflictual situations, where parallel execution should not be allowed.

Inspired by Lee and Matsikoudis [31], we use firing rules to define the semantics of components. This lets us define the semantics of each component in an input-output relation style. This is sensible for our application case, where we intend to use components that are directly implemented in hardware. Other application cases could require, instead, a notion of sequentiality: the behavior of a component is described by a sequential program. This corresponds to the general setting of Kahn Process Networks [22, 40, 42]. There, transitions of a component are of three possible, distinct kinds: consuming a token in an input channel, producing a token in an output channel and performing an internal action. Tripakis et al. [42] explains how non-atomic actors with these split transitions can serve in precisely analyzing timing properties.

In the literature of dataflow models, handling non-deterministic components – namely merges – is an important problem. This topic has been studied from two different perspectives: defining semantic models that support non-determinism, and finding the right balance between embracing non-determinism and maintaining determinacy. In our case, thanks to the small-step operational style of our semantics, defining the semantics of circuits with non-deterministic components is straightforward (even though achieving determinacy is not). In contrast, extending denotational semantics of KPN to non-deterministic actors is more involved; some extensions have been proposed by Broy [6], Russell [39]. Regarding the balance between non-determinism and determinacy, we prove our determinacy property only for safe usages of non-deterministic components, that never effectively exercise non-determinism. Recent work in HLS [20] propose to rely on a controlled, though observable, non-determinism to allow out-of-order replays of the same circuit, with an increased parallelism. The approach reuses the idea of colored tokens [16] to distinguish parallel executions of a same procedure. There, determinacy is temporarily broken, and then re-established through the use of so-called aligner components.

Relying on core languages or calculi to prove semantic properties, as we do with Cilan, is common to the field of formal verification. In particular, Faustini [21] switches to an IR similar to Cilan. Their IR uses two operators: a juxtaposition, corresponding to our parallel composition, and an iteration operator, corresponding to a combination of our self-composition and port remapping. We intentionally use constructs dedicated to specific aspects of circuits composition. This results in conceptually simple proofs, which decouple the various aspects as much as possible.

We deliberately made our two IR and their semantics as generic and simple as possible, mainly because they are thought to be mid-level compiler IR, and not circuit design languages. In particular, Cilan only contains enough constructs to be equivalent to Cigr. Many languages have been proposed [5, 18, 19, 29, 40, 41] which offer richer syntaxes. We made our IR generic, parameterized by a set of components, instead of directly embedding the components and their semantics in the IR. In particular, most of our IR syntax and semantics could be reused for other dataflow languages such as Pegasus [7] or the Program Dependence Web [8], by defining the firing rules of their respective sets of components.

Our work is a first step towards the verification of the functional correctness of an HLS compiler based on elastic circuits. We are not yet considering some other questions such as timing or scheduling-related properties. For these other questions, that go beyond compiler verification, other formal models may be more appropriate than our IR and their semantics. For example, Tripakis et al. [42] expresses properties on token consumption/production rates thanks to transitions dedicated to these actions. Other models like uninterpreted Petri Nets are also useful to study performance and
liveness properties [9, 12]. The dataflow circuits we present in this paper are a high-level model for elastic circuits, and thus do not include low-level aspects such as scheduling firing rules within one clock cycle [3, 13], avoiding combinational cycles [37], or reducing the resource usage [44]. While these are certainly key aspects of practical HLS, we leave these challenges for future work.

Existing mechanizations exist for higher-level models of dataflow, such as the synchronous languages Lustre [10] in the Vélus compiler [4] and Esterel [2]. For lower-level hardware circuit models, various hardware description languages (HDL) have been formalized. They range from elementary circuit representations, such as Coquet [5], to classical HDL like Verilog [23, 35], including also some more specific rule-based languages like Fe-Si [13] and Kôika [3], both derived from BlueSpec [1]. All of these works do not rely on dataflow circuits per se. The denotational semantics for KPN, as mechanized by Paulin-Mohring [36], does not include previously cited extensions to non-deterministic actors.

# 10 Conclusion and Future Work

Dataflow computing has a long and rich history, with a large spectrum of application domains. Our formalizing work, focusing on asynchronous dataflow circuits, is inspired from this rich heritage, both in theoretical and practical terms. Despite this vast body of foundational works and their recent successful applications in practical HLS compilation techniques, dataflow circuits have received little attention from a verified compilation point of view. We consider dataflow circuits as a key abstraction layer, used to bridge the gap between the source-level control-driven execution model and the hardware-level data-driven execution model.

Our work provides a formal semantics for dataflow circuits represented in two mid-level compiler IR with complementary objectives. Cigr is directly representing circuits as graphs of components, in a spirit similar to a control-flow graph IR for sequential imperative programs. Cilan, on the other hand, provides a structured construction of circuits as terms, and inductive reasoning principles. As such, Cilan is a useful proof-device for formal proofs of semantic meta-properties. Our semantic equivalence result allows for switching between both IR.

Our semantics is operational, and parameterized by an abstract definition of components, that we can then instantiate on concrete components, such as the one used in practical HLS compilers. Our extracted, executable interpreter for circuits in Cigr demonstrates the faithfulness of our semantic model: we are able to reproduce the observable behaviors of concrete, hardware circuits synthesized with Dynamatic. In addition to simple, stateless components, our semantics is able to deal with stateful components, and non-deterministic components.

On our abstract definition for components, we define formal criteria expressing fine-grained aspects related to non-determinism and parallelizability. From these criteria, we derive a formal proof for two important semantic meta-properties for dataflow circuits. In particular, we prove that our basic criteria expressed on components lift to whole-circuit behaviors, and imply trace determinacy for safe usages of non-determinism.

Our formal semantics for dataflow circuits is mechanized in Coq, and provides a first stepping stone towards a larger and challenging goal: the formal verification of HLS techniques based on elastic circuits, where circuits are dynamically scheduled. Our next step is to devise custom proof methodologies for the correctness of dataflow circuits rewritings, that are typical of dataflow circuits optimization phases. Additionally, we are currently reusing our work to provide a lower-level semantics for our IR, implementing the handshake protocol of elastic circuits, and ensuring the lack of combinational cycles. Finally, we plan on reusing our generic IR and semantics, and instantiate them for higher-level compilation phases, on the Program Dependence Web [8].
A Definition of Predicates · ↛$_{c}$ · , · ↛$_{in}$ · and · ↛$_{out}$ ·

Recall that predicate T ↛ G states that the circuit term T syntactically matches the circuit graph G. To define this predicate, we rely on the three following predicates : predicate T ↛ n c , predicate T ↛ n in ⃗ π and predicate T ↛ n,k out π . We give their formal definition below.

Predicate T ↛ n c states that c is a component identified by n in term T . Its definition is straightforward: we simply traverse the term to associate the identifier n to the basic component unit with the right identifier at a leaf of the term. This predicate is formally defined inductively as follows.

$$
\frac{\{n \mapsto (c, \vec{\pi}_i, \vec{\pi}_o)\} \rightsquigarrow_c^n c}{(\uparrow T) \rightsquigarrow_c^n c} \qquad \frac{T \rightsquigarrow_c^n c}{(\uparrow T) \rightsquigarrow_c^n c} \qquad \frac{T \rightsquigarrow_c^n c}{(\chi_{\omega_o}^{\omega_i} T) \rightsquigarrow_c^n c} \qquad \frac{T \rightsquigarrow_c^n c}{(T \star T') \rightsquigarrow_c^n c} \qquad \frac{T' \rightsquigarrow_c^n c}{(T \star T') \rightsquigarrow_c^n c}
$$

Predicate T ↛ n in ⃗ π states that, in term T, ⃗ π are the identifiers of the channels connected to the input ports of the component identified by n. Its definition presents no major difficulty either: we also traverse the term to find the basic component unit with the right identifier. This predicate is formally defined inductively as follows.

$$
\frac{\{n \mapsto (c, \vec{\pi}_i, \vec{\pi}_o)\} \rightsquigarrow_{\text{in}}^n \vec{\pi}_i}{(\uparrow T) \rightsquigarrow_{\text{in}}^n \vec{\pi}} \quad \frac{T \rightsquigarrow_{\text{in}}^n \vec{\pi}}{(\uparrow T) \rightsquigarrow_{\text{in}}^n \vec{\pi}} \quad \frac{T \rightsquigarrow_{\text{in}}^n c}{(\chi_{\omega_o}^{\omega_i} T) \rightsquigarrow_{\text{in}}^n c} \quad \frac{T \rightsquigarrow_{\text{in}}^n \vec{\pi}}{(T \star T') \rightsquigarrow_{\text{in}}^n \vec{\pi}} \quad \frac{T' \rightsquigarrow_{\text{in}}^n \vec{\pi}}{(T \star T') \rightsquigarrow_{\text{in}}^n \vec{\pi}}
$$

In Cilan, since no renaming occurs for input channels of self-composition operators, the input channel identifiers are the same for the self-composed term and for the bare term. Also, in a remapped term χ ω i ω o T, the interface of components is unchanged: only the interface of the term is modified. Hence, identifiers of input channels are the same in both the remapped term and the bare term.

Finally, predicate T ↛ n,k out π states that π is the identifier of the channel connected to the k-th output port of n in T . Contrary to the previous predicate, this one needs to take into account the renaming of output channel identifiers induced by self-composition in Cilan. This predicate is formally defined inductively as follows.

$$
\frac{\{n \mapsto (c, \vec{\pi}_i, \vec{\pi}_o)\} \rightsquigarrow_{\text{out}}^{n,k} (\vec{\pi}_o)_k}{(\uparrow_{\pi_1}^{\pi_2} T) \rightsquigarrow_{\text{out}}^{n,k} \pi_2} \qquad \frac{T \rightsquigarrow_{\text{out}}^{n,k} \pi_1}{(\uparrow_{\pi_1}^{\pi_2} T) \rightsquigarrow_{\text{out}}^{n,k} \pi_1} \qquad \frac{T \rightsquigarrow_{\text{out}}^{n,k} \pi}{(\uparrow_{\pi_1}^{\pi_2} T) \rightsquigarrow_{\text{out}}^{n,k} \pi} \qquad \frac{\pi \neq \pi_1}{\pi \neq \pi_2}
$$

There is no difficulty for basic component units, or parallel compositions of terms. For a term ↑ π 2 π 1 T, channel π 2 is the k-th output channel of component identified by n in ↑ π 2 π 1 T only if π 1 is the k-th output channel of n in T. Otherwise, π is connected to the same output port of the same component in both the self-composed term and the bare term. For a remapped term χ ω i ω o T, the previously explained principles still holds: only the interface of the term is modified by the remapping operator, and not the interface of components.

We define these three predicates on any possible Cilan term in a relational style. However, when T is well-formed, all component identifiers are unique: this makes these predicates functional.
## B Specification of toCilan

The translation toCilan converts a circuit graph $G$ into a circuit term $T$. Intuitively, toCilan works in three steps. First, it disconnects all components in the circuit graph. Then, it creates a term that is the parallel composition of all these (disconnected) components. Finally, it reconstructs the connections by combining remappings and self-composition operators.

Let us first describe the specification of toCilan in more details. To do so, we need to introduce the notation $\vec{l}[\vec{a} := \vec{b}]$. It applies to an identifier list $\vec{l}$ the substitutions given in the renaming map $\{a_k \mapsto b_k \mid k = 0 \dots |\vec{a}|\}$. For this substitution to be well-defined, $\vec{a}$ and $\vec{b}$ should have the same length, and $\vec{a} \cdot \vec{b}$ should contain no duplicate values.

The first step of toCilan disconnects all the components in the graph by renaming, using fresh identifiers, the output channels that are connecting components. Formally, we define a predicate disconnection($G, \vec{\pi}, \vec{\pi}', G'$) as follows, where we reuse, for Cigr, the notations previously introduced on Cilan. We write $G^\uparrow$ for the set of internal channels of $G$, and $G^{\Pi s}$ for its complete set of channel identifiers.

**Definition B.1.** A circuit disconnection disconnection($G, \vec{\pi}, \vec{\pi}', G'$) between graphs $G, G' \in$ Cigr and channel identifier lists $\vec{\pi}$ and $\vec{\pi}'$ is defined as follows:

* Identifiers in $\vec{\pi}$ are connecting components of $G: \forall x, x \in \vec{\pi} \iff x \in G^\uparrow$.

* Identifiers in $\vec{\pi}'$ are fresh in $G: \vec{\pi}' \cap G^{\Pi s} = \emptyset$.

* $G'$ is disconnected: $\forall n n' k k', G'[n]^{\text{in}}[k] \neq G'[n']^{\text{out}}[k']$.

* $G'$ is a renaming of $G$ on its output channels: for all component identifiers $n$, we have $G'[n]^{\text{out}} = G[n]^{\text{out}}[\vec{\pi} := \vec{\pi}']$, but component and input channel identifiers are untouched i.e., $G'[n]^c = G[n]^c$ and $G'[n]^{\text{in}} = G[n]^{\text{in}}$.

We then rely on this definition to specify the toCilan translation as follows.

**LEMMA B.2 (SPECIFICATION OF toCilan).** Let $G \in$ Cigr such that $wf_{Cigr} G$. There exists an auxiliary graph $G'$ and channel identifiers $\vec{\pi}$ and $\vec{\pi}'$ such that

* disconnection($G, \vec{\pi}, \vec{\pi}', G'$)

* toCilan($G$) = $\mathop{\mathrm{disconnection}}(G, \vec{\pi}, \vec{\pi}', G')$

where $\star$ is the parallel composition operator generalized to a list of identifiers and $\mathop{\mathrm{disconnection}}(G, \vec{\pi}, \vec{\pi}', G')$ combines self-compositions and remappings to connect the k-th element of $\vec{\pi}'$ to the k-th element of $\vec{\pi}$.

Based on the above specification of toCilan, we then prove that toCilan yields a well-formed, syntactically matching term (Lemma 7.3) in three steps. First, we prove that the disconnection relation entails the well-formedness of the disconnected graph $G'$, by induction on the number of the components of the initial graph $G$. Second, we prove that the parallel composition of all components of $G'$, $(\star_n\{n \mapsto G'[n]\})$, is a well-formed term, and that $(\star_n\{n \mapsto G'[n]\}) \rightsquigarrow G'$. We do so by induction on the number of the components in $G'$. Finally, we prove that the term $\mathop{\mathrm{disconnection}}(\star_n\{n \mapsto G'[n]\})$ is well-formed, and that $\mathop{\mathrm{disconnection}}(\star_n\{n \mapsto G'[n]\}) \rightsquigarrow G$. This time, we prove it by induction on $\vec{\pi}$, i.e., the connections of the initial circuit graph $G$.

## Data-Availability Statement

Our complete Coq formal development and our experimental setup validating our formal semantics are available online as a reusable artifact [28], with which all claims and experimental results presented in this paper can be reproduced.
## References

[1] Lennart Augustsson, Jacob Schwartz, and Rishiyur S Nikhil. 2001. Bluespec Language Definition. *Sandburst Corp* (2001).

[2] Gérard Berry and Lionel Rieg. 2022. Towards Coq-verified Esterel Semantics and Compiling. doi:10.48550/arXiv.1909.12582 arXiv:1909.12582 [cs]

[3] Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, and Arvind. 2020. The Essence of Bluespec: A Core Language for Rule-Based Hardware Design. In *Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020)*. Association for Computing Machinery, New York, NY, USA, 243–257. doi:10.1145/3385412.3385965

[4] Timothy Bourke, Lélio Brun, and Marc Pouzet. 2019. Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset. *Proceedings of the ACM on Programming Languages* 4, POPL (Dec. 2019), 44:1–44:29. doi:10.1145/3371112

[5] Thomas Braibant. 2011. Coquet: A Coq Library for Verifying Hardware. In *Certified Programs and Proofs*, Jean-Pierre Jouannaud and Zhong Shao (Eds.). Springer, Berlin, Heidelberg, 330–345. doi:10.1007/978-3-642-25379-9_24

[6] Manfred Broy. 1988. Nondeterministic Data Flow Programs: How to Avoid the Merge Anomaly. *Science of Computer Programming* 10, 1 (Feb. 1988), 65–85. doi:10.1016/0167-6423(88)90016-0

[7] M. Budiu and S. Goldstein. 2002. Pegasus: An Efficient Intermediate Representation.

[8] P. L. Campbell, K. Krishna, and R. A. Ballance. 1993. Refining and Defining the Program Dependence Web. (May 1993).

[9] Josep Carmona, Jordi Cortadella, Mike Kishinevsky, and Alexander Taubin. 2009. Elastic Circuits. *IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems* 28, 10 (2009), 1437–1455. doi:10.1109/TCAD.2009.2030436

[10] P. Caspi, D. Pilaud, N. Halbwachs, and J. A. Plaice. 1987. LUSTRE: A Declarative Language for Real-Time Programming. In *Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL '87)*. Association for Computing Machinery, New York, NY, USA, 178–188. doi:10.1145/41625.41641

[11] Jianyi Cheng, Lana Josipović, 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–252. doi:10.1109/FPL57034.2022.00045

[12] 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–203. doi:10.1109/FCCM51124.2021.00031

[13] Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind. 2017. Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification. *Proceedings of the ACM on Programming Languages* 1, ICFP (Aug. 2017), 24:1–24:30. doi:10.1145/3110268

[14] Jordi Cortadella, Mike Kishinevsky, and Bill Grundmann. 2006. Synthesis of Synchronous Elastic Architectures. In *Proceedings of the 43rd Annual Design Automation Conference (DAC '06)*. Association for Computing Machinery, New York, NY, USA, 657–662. doi:10.1145/1146909.1147077

[15] Dennis. 1980. Data Flow Supercomputers. *Computer* 13, 11 (1980), 48–56. doi:10.1109/MC.1980.1653418

[16] Jack B. Dennis. 1974. First Version of a Data Flow Procedure Language. In *Programming Symposium (Lecture Notes in Computer Science)*, B. Robinet (Ed.). Springer, Berlin, Heidelberg, 362–376. doi:10.1007/3-540-06859-7_1145

[17] Jack B. Dennis and David P. Misunas. 1974. A preliminary architecture for a basic data-flow processor. In *Proceedings of the 2nd Annual Symposium on Computer Architecture (ISCA '75)*. Association for Computing Machinery, New York, NY, USA, 126–132. doi:10.1145/642089.642111

[18] W. Dosch. 2005. Designing Combinational Circuits with List Homomorphisms. In *Third ACIS Int'l Conference on Software Engineering Research, Management and Applications (SERA '05)*. 288–297. doi:10.1109/SERA.2005.35

[19] Stephen A. Edwards, Richard Townsend, Martha Barker, and Martha A. Kim. 2019. Compositional Dataflow Circuits. *ACM Transactions on Embedded Computing Systems* 18, 1 (Jan. 2019), 5:1–5:27. doi:10.1145/3274280

[20] Ayatallah Elakhras, Andrea Guerrieri, Lana Josipovic, and Paolo Ienne. 2024. Survival of the Fastest: Enabling More Out-of-Order Execution in Dataflow Circuits. In *Proceedings of the 2024 ACM/SIGDA International Symposium on Field Programmable Gate Arrays (FPGA '24)*. Association for Computing Machinery, New York, NY, USA, 44–54. doi:10.1145/3626202.3637556

[21] Antony Azio Faustini. 1982. *The Equivalence of an Operational and a Denotational Semantics for Pure Dataflow*. Ph. D. Dissertation. University of Warwick. Department of Computer Science.

[22] Marc Geilen and Twan Basten. 2010. Kahn Process Networks and a Reactive Extension. In *Handbook of Signal Processing Systems*, Shuvra S. Bhattacharyya, Ed F. Deprettere, Rainer Leupers, and Jarmo Takala (Eds.). Springer US, Boston, MA, 967–1006. doi:10.1007/978-1-4419-6345-1_34

[23] Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. 2021. Formal verification of high-level synthesis. *Proc. ACM Program. Lang.* 5, OOPSLA, Article 117 (oct 2021), 30 pages. doi:10.1145/3485494
[24] Lana Josipović, Radhika Ghosal, and Paolo Ienne. 2018. Dynamically Scheduled High-level Synthesis. In Proceedings of the 2018 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays (FPGA '18). Association for Computing Machinery, New York, NY, USA, 127–136. doi:10.1145/3174243.3174264

[25] Lana Josipović, Andrea Guerrieri, and Paolo Ienne. 2022. From C/C++ Code to High-Performance Dataflow Circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 41, 7 (July 2022), 2142–2155. doi:10.1109/TCAD.2021.3105574

[26] Gilles Kahn. 1974. The Semantics of a Simple Language for Parallel Programming. (1974).

[27] Richard M. Karp and Rayamond E. Miller. 1966. Properties of a Model for Parallel Computations: Determinacy, Termination, Queueing. SIAM J. Appl. Math. 14, 6 (Nov. 1966), 1390–1411. doi:10.1137/0114108

[28] Tony Law, Delphine Demange, and Sandrine Blazy. 2025. A Mechanized Semantics for Dataflow Circuits. doi:10.5281/zenodo.14938628

[29] P. Le Guernic, A. Benveniste, P. Bournai, and T. Gautier. 1986. Signal-A Data Flow-Oriented Language for Signal Processing. IEEE Transactions on Acoustics, Speech, and Signal Processing 34, 2 (April 1986), 362–374. doi:10.1109/TASSP.1986.1164809

[30] E.A. Lee and T.M. Parks. 1995. Dataflow process networks. Proc. IEEE 83, 5 (1995), 773–801. doi:10.1109/5.381846

[31] Edward A. Lee and Eleftherios Matsikoudis. 2009. The Semantics of Dataflow with Firing. In From Semantics to Computer Science (1 ed.), Yves Bertot, Gérard Huet, Jean-Jacques Lévy, and Gordon Plotkin (Eds.). Cambridge University Press, 71–94. doi:10.1017/CBO9780511770524.005

[32] Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52, 7 (Jul 2009), 107–115. doi:10.1145/1538788.1538814

[33] David B. MacQueen. 2009. Kahn networks at the dawn of functional programming. Cambridge University Press, 95–138. doi:10.1017/CBO9780511770524.006

[34] Mentor Graphics. 2020. ModelSim.

[35] Patrick Meredith, Michael Katelman, José Meseguer, and Grigore Roșu. 2010. A Formal Executable Semantics of Verilog. In Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010). 179–188. doi:10.1109/MEMCOD.2010.5558634

[36] Christine Paulin-Mohring. 2009. A Constructive Denotational Semantics for Kahn Networks in Coq. In From Semantics to Computer Science (1 ed.), Yves Bertot, Gérard Huet, Jean-Jacques Lévy, and Gordon Plotkin (Eds.). Cambridge University Press, 383–414. doi:10.1017/CBO9780511770524.018

[37] Adam Procter, William L. Harrison, Ian Graves, Michela Becchi, and Gerard Allwein. 2015. Semantics Driven Hardware Design, Implementation, and Verification with ReWire. In Proceedings of the 16th ACM SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2015 CD-ROM (LCTES'15). Association for Computing Machinery, New York, NY, USA, 1–10. doi:10.1145/2670529.2754970

[38] J. E. Rodrigues. 1969. A GRAPH MODEL FOR PARALLEL COMPUTATIONS. Technical Report. USA.

[39] James R. Russell. 1989. On Oraclizable Networks and Kahn's Principle. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '90). Association for Computing Machinery, New York, NY, USA, 320–328. doi:10.1145/96709.96742

[40] Eugene W. Stark. 1995. AN ALGEBRA OF DATAFLOW NETWORKS. Fundamenta Informaticae 22, 1-2 (Jan. 1995), 167–185. doi:10.3233/FI-1995-22128

[41] Gheorghe Ștefănescu. 2000. Network Algebra. Springer, London, Berlin, Paris. doi:10.1007/978-1-4471-0479-7

[42] Stavros Tripakis, Rhishikesh Limaye, Kaushik Ravindran, Guoqiang Wang, Hugo Andrade, and Arkadeb Ghosal. 2016. Tokens vs. Signals: On Conformance between Formal Models of Dataflow and Hardware. Journal of Signal Processing Systems 85, 1 (Oct. 2016), 23–43. doi:10.1007/s11265-015-0971-y

[43] Nam Sung Woo. 1983. A Pragmatic Parallel Computation Model and Its Computer Architecture. Ph. D. Dissertation. University of Maryland.

[44] Jiahui Xu, Emmet Murphy, Jordi Cortadella, and Lana Josipovic. 2023. Eliminating Excessive Dynamism of Dataflow Circuits Using Model Checking. In Proceedings of the 2023 ACM/SIGDA International Symposium on Field Programmable Gate Arrays. ACM, Monterey CA, USA, 27–37. doi:10.1145/3543622.3573196

Received 2024-10-16; accepted 2025-02-18