一句话：在 Lean 4 中建立数据流电路的图精化元理论，并形式化验证引入乱序执行的循环重写，性能与未验证方法持平。
高层综合（HLS）工具能从命令式程序自动生成硬件，而对最不规则的程序，生成数据流电路的 HLS 工具通过借鉴处理器架构中的乱序执行与推测等思想获得良好性能。然而这些变换过于复杂，难以推理，容易引入隐蔽缺陷，从而阻碍其在保守产业中的采用。本文提出 Graphiti——一个嵌入 Lean 4 证明助手的框架，用于对这类 HLS 工具核心的数据流电路进行形式化推理与操纵。作者发展了图精化（graph refinement）元理论，据此验证了一个通用数据流电路重写算法，并形式化验证了将乱序执行引入数据流电路的循环重写。评估表明，该已验证优化流水线相对顺序执行的 HLS 流程取得 2.1× 加速，相对生成静态状态机的已验证 HLS 工具取得 5.8× 加速，且与已有的未验证乱序执行方法性能相当。Graphiti 是迈向全验证数据流 HLS 流程的一步，同时也可作为可扩展的已验证优化引擎集成进现有数据流 HLS 编译器。
High-level synthesis (HLS) tools automatically synthesise hardware from imperative programs and have seen a significant rise in adoption in both industry and academia. To deliver high-quality hardware designs for increasingly general purpose programs, HLS compilers have to become more aggressive. For the most irregular programs, HLS tools generating dataflow circuits show promising performance by adapting and specializing key ideas from processor architectures, like out-of-order execution and speculation. However, the complexity of these transformations makes them difficult to reason about, increasing the risk of subtle bugs and potentially delaying their adoption in a conservative industry where bugs can be extremely costly. This paper introduces Graphiti, a framework embedded in the Lean 4 proof assistant designed to formally reason about and manipulate dataflow circuits at the core of these HLS tools. We develop a metatheory of graph refinement that allows us to verify a general-purpose dataflow circuit rewriting algorithm. Using this framework, we formally verify a loop rewrite that introduces out-of-order execution into a dataflow circuit. Our evaluation shows that the resulting verified optimization pipeline achieves a 2.1× speedup over the in-order HLS flow and a 5.8× speedup over a verified HLS tool generating a static state machine. We also show that it achieves the same performance compared to an existing unverified approach which introduces out-of-order execution. Graphiti is a step toward a fully-verified HLS flow targeting dataflow circuits. In the interim, it can serve as an extensible, verified, optimizing engine that can be integrated into existing dataflow HLS compilers.
@inproceedings{HerklotzECIJB26,
title = {Graphiti: Formally Verified Out-of-Order Execution in Dataflow Circuits},
author = {Yann Herklotz and Ayatallah Elakhras and Martina Camaioni and Paolo Ienne and Lana Josipović and Thomas Bourgeat},
booktitle = {ASPLOS},
year = {2026},
doi = {10.1145/3779212.3790166}
}