ElasticMiter: Formally Verified Dataflow Circuit Rewrites

A growing way to turn software into custom chips produces dataflow circuits, whose parts run whenever their data is ready rather than on a fixed clock — which means the usual way of proving that an optimized circuit still behaves like the original, comparing them cycle by cycle, wrongly rejects perfectly good optimizations; this work from ETH Zurich and EPFL rethinks what equivalence should mean for these circuits (the same stream of data values, whenever it arrives), builds ElasticMiter to prove it automatically, and uses it to certify a library of circuit simplifications that cut latency by about a quarter with a formal correctness guarantee.

The argument in one glance

Problem

Dataflow circuits break the standard notion of equivalence

High-level synthesis increasingly compiles software into dataflow circuits, whose units run whenever their data arrives rather than on a fixed clock. To optimize such a circuit into a simpler equivalent one and prove it correct, you need an equivalence check — but the standard one demands identical outputs every clock cycle, which dataflow circuits, being latency-insensitive, do not satisfy even when they compute the same thing.
What people did

Use standard sequential equivalence verification

Apply the mature sequential-equivalence checkers used for ordinary circuits, which prove two circuits produce the same outputs on every clock cycle.
Why it fell short

Cycle-by-cycle equality is the wrong test

Two dataflow circuits that produce the same data values but at different times are functionally equivalent and interchangeable, yet sequential equivalence rejects them because their per-cycle outputs differ. Being too strict, it cannot capture latency-insensitivity, so it blocks the development of formally verified dataflow circuit transformations.
This paper's idea

Verify equivalence on token sequences, not cycles (ElasticMiter)

ElasticMiter defines equivalence as producing and consuming the same sequence of valid tokens, regardless of when — a notion that fits latency-insensitive circuits and reduces to finite-state model checking. It proves two dataflow circuits equivalent in general or under conditions inherited from the source code, and is used to verify a library of small, local rewrite rules that shrink circuits. As a pass in an open-source HLS compiler, the verified rewrites cut latency by about 24 percent and FPGA flip-flop resources by about 14 percent.

Why this problem is worth solving

Turning software into custom hardware is powerful, and a flexible new circuit style is making it more so.

High-level synthesis, or HLS, is the technology of compilers that turn ordinary high-level programs — written in a language like C or C-plus-plus — into hardware circuits, giving software developers a way to program reconfigurable chips called FPGAs without designing hardware by hand. A modern and increasingly popular target for these compilers is the dataflow circuit. Instead of a rigid design where every operation happens at a compiler-fixed clock cycle, a dataflow circuit is built from many fine-grained units that communicate by passing data to one another over bidirectional handshake signals. The crucial difference is timing: when data is exchanged between units is not predetermined by the compiler but decided at runtime, depending on the actual data and control outcomes. A unit fires when its inputs are ready and the receiver is ready to accept, and otherwise waits. This scheduling flexibility, together with features like speculation and multithreaded execution, gives dataflow circuits significant performance advantages over conventional HLS on irregular, control-dominated applications — which is exactly why the approach is being actively developed and refined.

But as these compilers grow more sophisticated, a basic verification tool they need turns out not to exist.

Like any compiler, an HLS tool wants to optimize what it produces — here, to replace an expensive dataflow circuit with a simpler one that computes the same thing, and to prove the two are equivalent so the optimization is trustworthy. For ordinary synchronous circuits, the standard tool for this is sequential equivalence: two circuits are equivalent if they produce identical outputs on every single clock cycle, and mature automated checkers verify exactly this. The problem is that dataflow circuits are latency-insensitive, and sequential equivalence is the wrong test for them. Because a dataflow unit fires whenever its data is ready, two dataflow circuits can produce the same data values at different times and still be completely interchangeable — swapping one for the other changes only when tokens are produced and consumed, never the values themselves. Sequential equivalence cannot see this: it demands cycle-by-cycle equality, so it declares two latency-insensitive-equivalent circuits unequal merely because their timing differs. The right notion is more like software verification, where what matters is that two programs compute the same values, not that they take exactly the same number of cycles. Without an equivalence check that captures this, formally verified dataflow transformations were simply out of reach.

What people did before, and where it broke

Use standard sequential equivalence checkers. Apply the mature tools that prove two circuits produce identical outputs every clock cycle. Where it broke. This is too strict for dataflow circuits, rejecting latency-insensitive-equivalent circuits because their timing differs, so it cannot verify the transformations that matter.
Optimize dataflow circuits without a correctness proof. Apply simplifications and trust that they preserve behavior. Where it broke. Without a proof, aggressive rewrites risk silently changing behavior, which is unacceptable for hardware that must be correct.
Reuse verification meant for standard HLS. Borrow formal strategies developed for conventional HLS flows. Where it broke. Those strategies do not capture the latency-insensitive nature of dataflow computation, so they miss the very property that makes dataflow equivalence special.
The gap. No verification framework captured latency-insensitive equivalence in a way an automatic tool could check, and none had been used to prove dataflow circuit transformations correct. Providing both is what ElasticMiter does.

How ElasticMiter works

From cycle-by-cycle equality to verified token-sequence equivalence

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Redefine equivalence to match what dataflow actually guarantees. ElasticMiter’s foundation is a new, practical definition of equivalence: two dataflow circuits are equivalent when they produce and consume the same sequence of valid tokens, regardless of the exact cycles on which those exchanges happen — capturing latency-insensitivity, which the standard cycle-by-cycle notion cannot. Recognizing that the standard, inherited notion of correctness simply does not fit a new kind of system, and replacing it with a precise definition built for that system’s real behavior, is the same move the disaggregated-memory work covered elsewhere on this site makes, discarding the single-machine assumptions that break in the new setting and writing down an exact model suited to how the new hardware actually behaves.

Make the new equivalence something a machine can prove. Rather than argue equivalence informally, ElasticMiter frames its definition so the question reduces to finite-state model checking — an automatic, exhaustive search that either proves two circuits equivalent or finds a counterexample, in general or under conditions the source code guarantees. Turning a correctness question into a form that an automated tool can check exhaustively against a precise specification, rather than trusting hand argument, is the same discipline the GPU memory-model work covered elsewhere on this site follows, casting the rules precisely enough that a checker can decide whether real behavior conforms, so verification is mechanical and trustworthy.

Verify small local rules once, then optimize freely. Because whole-circuit proofs would be intractable, ElasticMiter’s rewrites are small and localized, each verified a single time by the framework in acceptable runtime; once a rule is proven to preserve token-sequence equivalence, the compiler can apply it wherever the pattern appears, confident every result is correct. Proving a compact hardware transformation correct once so that all of its many applications are trustworthy by construction is the same strategy the verified-pipeline-protocol work covered elsewhere on this site takes, establishing the correctness of a hardware transformation formally so that its use does not have to be re-justified each time it is applied.

Following a rewrite through ElasticMiter

Verifying and applying a circuit simplification

A trace of ElasticMiter proving one rewrite rule and applying it, following the paper's framework.

Step 1 of 5

A compiler emits redundant dataflow logic

An HLS compiler produces a dataflow circuit that is correct but carries redundant, area-heavy steering logic — a candidate for simplification into something equivalent but cheaper.

Dataflow circuits are known to suffer from such area overheads.

Why it works

The right equivalence matches what dataflow actually guarantees. Because dataflow circuits are latency-insensitive and only the token values matter, not their timing → an equivalence demanding cycle-by-cycle equality rejects valid optimizations → so defining equivalence on token sequences is what lets real transformations be proven correct.
Token-sequence equivalence can be model-checked. Because the new definition is framed to be compatible with finite-state model checking → an automatic tool can exhaustively prove two circuits equivalent or produce a counterexample → so verification is rigorous and needs no hand-written proof per circuit.
Small local rules are cheap to verify but broadly useful. Because each rewrite pattern is small and localized → the framework can verify it in acceptable runtime → so a rule proven once can be applied everywhere it matches, amortizing the verification cost.
Context lets more optimizations be proven. Because HLS circuits inherit behavioral constraints from their source code → verifying under those conditions proves rewrites that would not be valid in the fully general case → so more aggressive simplifications become provably safe.
Verified rewrites give optimization without risk. Because every applied rule is proven equivalent → the optimizer can shrink area and latency with no chance of changing behavior → so the compiler gains a correctness guarantee alongside its speedups.

What it costs (trade-offs and scope)

Rewrites must stay small to be verifiable. The framework verifies small, localized patterns because whole-circuit equivalence checking would not scale. This keeps verification tractable but means the optimization power comes from composing many small proven rules rather than proving large transformations directly.
Model checking has inherent limits. Finite-state model checking is exhaustive but bounded by state-space size, so the approach depends on the patterns and their token behavior remaining small enough to check. It inherits the usual scalability constraints of model checking.
The equivalence notion is specific to latency-insensitive circuits. The token-sequence definition is designed for dataflow, handshake-based circuits. It is exactly the right tool there, but it is a specialized notion, not a drop-in replacement for sequential equivalence in ordinary synchronous design.
Context-based proofs rest on assumptions. Verifying a rewrite under conditions inherited from the source code proves more optimizations, but the guarantee then holds only when those conditions actually hold, so the constraints the source software imposes must be captured correctly.
The gains are measured on one compiler and its benchmarks. The reported 24 percent latency and 14 percent flip-flop reductions come from implementing the pass in a specific open-source HLS compiler on its benchmarks; other circuits and compilers would shift the numbers.
It optimizes datapath steering logic, within scope. The work targets simplifying the datapaths and steering logic of HLS-produced dataflow circuits; it is a foundation for verified dataflow HLS rather than a complete verified compiler on its own.

The evaluation

Three ways to handle dataflow circuit optimization and its correctness

Property	Sequential equivalence	Unverified rewrites
Recognizes latency-insensitive equivalence
Proves rewrites correct	Rejects valid ones
Handles source-code conditions	Not applicable	Not applicable
Automatic, no hand proof	Yes, but wrong notion	Not applicable
Outcome	Blocks dataflow optimization

Three ways to handle the optimization of HLS-produced dataflow circuits and its correctness, as framed by the paper. Standard sequential equivalence proves two circuits identical cycle by cycle, but that is too strict for latency-insensitive dataflow circuits and rejects valid optimizations. Optimizing without a proof risks silently changing behavior. ElasticMiter instead defines equivalence as producing and consuming the same sequence of valid tokens regardless of timing, reduces this to finite-state model checking that an automatic tool settles exhaustively, and can verify equivalence in general or under behavioral conditions inherited from the source code. Using it, the authors verify a library of small, local graph-rewrite rules that simplify dataflow steering logic, then implement them as a pass in Dynamatic, an open-source MLIR-based HLS compiler that converts C to dataflow circuits. The verified pass yields a 24 percent mean reduction in latency and a 14 percent reduction in FPGA flip-flop resources, with the resulting circuits provably equivalent to those of a state-of-the-art HLS compiler. This is the first work to formally verify dataflow circuit transformations.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

ElasticMiter is a foundational contribution that fills a real and specific gap in hardware compilation. Dataflow circuits are an increasingly important target for high-level synthesis, valued because their units run whenever data is ready rather than on a fixed clock, but that very latency-insensitivity broke the standard tool for proving optimizations correct: sequential equivalence demands identical outputs every cycle, which two interchangeable dataflow circuits simply do not provide. The paper’s central insight is to redefine equivalence to fit the domain — two circuits are equivalent if they produce and consume the same sequence of valid tokens, whenever those exchanges happen — and, crucially, to frame that definition so it reduces to finite-state model checking, making it something an automatic tool can prove exhaustively. On top of the verifier, the authors build a practical payoff: a library of small, local rewrite rules that simplify the area-heavy steering logic dataflow circuits tend to accumulate, each verified once and then applied freely, delivering a 24 percent mean latency reduction and 14 percent fewer flip-flops in a real open-source HLS compiler, with the results provably equivalent to a state-of-the-art baseline. Read the scope precisely. The approach relies on rewrites staying small and localized to keep model checking tractable, so power comes from composing many small proven rules rather than verifying large transformations directly; the equivalence notion is specialized to latency-insensitive circuits; context-based proofs hold only under the source-code conditions they assume; and the numbers are from one compiler and its benchmarks. The durable idea is that when a new kind of system breaks an old correctness criterion, the fix is not to force the old test but to define the right one — precisely enough that a machine can check it — and that doing so unlocks a whole class of previously unprovable, and therefore previously unsafe, optimizations.

Background

Why defining the right formal notion, then automating it, keeps paying off

It helps to see ElasticMiter within a broad pattern in systems and hardware: progress often hinges not on a faster algorithm but on getting a definition right — pinning down precisely what correctness means for a new kind of artifact — and then making that definition mechanically checkable so a tool, not a human, does the reasoning. Here the artifact is a latency-insensitive circuit and the definition is token-sequence equivalence; the payoff is that optimizations which were unprovable, and so unsafe to apply, become provably correct. The speculative-execution testing work covered elsewhere on this site reflects the same instinct in security, defining exactly what a processor is permitted to leak and then checking real behavior against that definition automatically, so that subtle violations are caught by machinery rather than missed by inspection. The common thread is that in domains where mistakes are costly and behavior is subtle — concurrent hardware, speculative processors, latency-insensitive circuits — informal reasoning is not enough; the winning move is a precise, checkable specification paired with an automated checker, and the biggest wins come the moment such a specification finally exists. Once it does, aggressive optimization and rigorous correctness stop being in tension, because every transformation carries a proof. As hardware compilation grows more ambitious, the ability to state the right equivalence and let a model checker enforce it is likely to become a standard part of trustworthy tool flows rather than a research novelty.

If you remember only three things

1. High-level synthesis compilers turn software (in a language like C) into hardware circuits for FPGAs, and dataflow circuits are an increasingly popular target: they are built from fine-grained units communicating over handshake signals, where the timing of each data exchange is decided at runtime rather than fixed by the compiler, giving big speedups on irregular, control-heavy code. These compilers need to optimize their circuits into simpler equivalent ones and prove the optimizations correct, but the standard verification tool, sequential equivalence, requires identical outputs on every clock cycle — which latency-insensitive dataflow circuits do not provide even when interchangeable, since two of them can produce the same values at different times. This mismatch blocked formally verified dataflow transformations.
2. ElasticMiter devises a practical definition of equivalence that fits dataflow: two circuits are equivalent if they produce and consume the same sequence of valid tokens (handshake-completed data), regardless of exactly when. It builds on latency-insensitive design theory to make this definition compatible with model checking, and provides a framework that proves two dataflow circuits equivalent either regardless of their surroundings or under behavioral conditions inherited from the source software, by reducing the question to finite-state model checking that an automatic tool settles exhaustively. Because whole-circuit proofs would not scale, its rewrites are small and localized, each verified once and then applied wherever the pattern matches.
3. Using ElasticMiter, the authors verify a library of graph-rewrite rules that simplify the area-heavy steering logic of HLS-produced dataflow circuits, and implement them as an optimization pass in Dynamatic, an open-source MLIR-based HLS compiler. The verified pass achieves a 24 percent mean reduction in latency and a 14 percent reduction in FPGA flip-flop resources, with the results provably equivalent to a state-of-the-art HLS compiler. This is the first work to formally verify dataflow circuit transformations. Scope: rewrites must stay small for model checking to scale, the equivalence notion is specialized to latency-insensitive circuits, context-based proofs hold only under their assumed conditions, and the numbers reflect one compiler and its benchmarks. The durable lesson is that when a new system breaks an old correctness criterion, the fix is to define the right one precisely enough for a machine to check, which unlocks optimizations that were previously unprovable and therefore unsafe.

Check yourself

Check your understanding

1. What makes dataflow circuits different, and why does that break standard equivalence checking?
2. What definition of equivalence does ElasticMiter use, and why is it the right one?
3. How does ElasticMiter make verification practical, and why are the rewrite rules kept small?
4. What did the authors build with ElasticMiter, and what are the results?

Sources

The paper is “ElasticMiter: Formally Verified Dataflow Circuit Rewrites” by Ayatallah Elakhras, Jiahui Xu, Martin Erhart, Paolo Ienne, and Lana Josipovic, published at ASPLOS 2025, DOI 10.1145/3676641.3715993. The authors are at ETH Zurich and EPFL.

This explainer is based on the full text of the paper, obtained as the open-access (CC-BY) author copy hosted by the authors’ research group. The problem framing (high-level synthesis compiling C to circuits for FPGAs, dataflow circuits built from fine-grained units communicating over handshake signals with runtime-determined timing, their latency-insensitivity, and the incompatibility of standard sequential equivalence — which requires identical outputs on every clock cycle — with latency-insensitive dataflow, illustrated by circuits that produce the same token values at different times), the contributions (a formal definition of latency-insensitive equivalence based on producing and consuming the same sequence of valid tokens, made compatible with model checking; a framework proving two dataflow circuits equivalent regardless of their surroundings or under behavioral conditions inherited from the source code, by reduction to finite-state model checking; a set of small, localized graph-rewrite rules that reduce the area and latency of HLS-produced dataflow circuits, each verified once with the framework; and their implementation as a compiler optimization pass in Dynamatic, an open-source MLIR-based HLS compiler), and the results (a 24 percent mean reduction in latency and a 14 percent reduction in FPGA flip-flop resources, with circuits provably equivalent to a state-of-the-art HLS compiler, and the claim of being the first to formally verify dataflow circuit transformations) are all drawn directly from the paper. Background explanations of high-level synthesis, dataflow and latency-insensitive circuits, sequential equivalence, model checking, and graph rewriting are standard and provided to make the paper’s contribution understandable.