The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Mechanized semantics for circuits: from dataflow to hardware
High-level synthesis (HLS) is a method in which a hardware design is produced from a high-level specification, generally written in C. It thus involves two different execution models: as inputs, sequential programs driven by their control flow, and as outputs, parallel circuits driven by their data flows. Dynamic scheduling techniques improve the use of hardware parallelism when transitioning between both models. This thesis is a first step in the design of a dynamic-scheduling HLS compiler, formally verified in the Rocq proof assistant. Our work focuses on a circuit representation that enables such dynamism, dataflow circuits, which we formalize at two levels: their specification at dataflow level, and their implementation at hardware level. We study two equivalent views for circuits: a graphical representation naturally suitable for compilers, and an inductive language simplifying reasonings and letting us prove semantic meta-properties, notably semantic preservation. We test the validity of our work against Dynamatic, a dynamic-scheduling HLS tool that also uses dataflow circuits.
A copy is held
pdf, 4.4 MB. Not published — it may be under
copyright. The facts and links here are.
@phdthesis{law2026mechanized,
title = {Mechanized semantics for circuits: from dataflow to hardware},
author = {Tony Law},
year = {2026},
school = {Université de Rennes},
doi = {10.70675/33859af0z9c09z423dzb345z62ae1ec51d10},
}