WG211/M24Blazy

This talk proposes a mechanized formal semantics for
 dataflow circuits: rather than following a static schedule
 predetermined at generation time, the execution of the components in
 a circuit 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 a 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.