一句话：提出首个形式化验证dataflow电路变换的框架ElasticMiter，并用图重写证明所得电路与原电路等价。
Dataflow电路具有延迟不敏感特性，长期用于异步/同步设计，近期成为高层次综合（HLS）编译器的目标。然而，如何系统变换与优化其数据通路并保持功能等价仍缺乏机制。核心挑战是等价验证：延迟不敏感特性与标准顺序等价不兼容，现有顺序等价验证策略无法直接使用，也阻碍形式化验证的数据流电路变换。本文提出通用框架ElasticMiter，用于验证延迟不敏感电路的等价性；并开发图重写系统，将dataflow电路系统地转换为更简单的电路，再用该框架验证重写模式，证明所得电路与原电路等价。该工作首次形式化验证dataflow电路变换，为构建形式化验证的数据流HLS编译器奠定基础。
Dataflow circuits have been studied for decades as a way to implement both asynchronous and synchronous designs, and, more recently, have attracted attention as the target of high-level synthesis (HLS) compilers. Yet, little is known about mechanisms to systematically transform and optimize the datapaths of the obtained circuits into functionally equivalent but simpler ones. The main challenge is that of equivalence verification: The latency-insensitive nature of dataflow circuits is incompatible with the standard notion of sequential equivalence, which prevents the direct usage of standard sequential equivalence verification strategies and hinders the development of formally verified dataflow circuit transformations in HLS. In this paper, we devise a generic framework for verifying the equivalence of latency-insensitive circuits. To showcase the practical usefulness of our verification framework, we develop a graph rewriting system that systematically transforms dataflow circuits into simpler ones. We employ our framework to verify our graph rewriting patterns and thus prove that the obtained circuits are equivalent to the original ones. Our work is the first to formally verify dataflow circuit transformations and is a foundation for building formally verified dataflow HLS compilers.
@inproceedings{ElakhrasXEIJ25,
title = {ElasticMiter: Formally Verified Dataflow Circuit Rewrites},
author = {Ayatallah Elakhras and Jiahui Xu and Martin Erhart and Paolo Ienne and Lana Josipovi?},
booktitle = {ASPLOS},
year = {2025},
doi = {10.1145/3676641.3715993}
}