Formal Reasoning on Dataflow Circuits
Event details
| Date | 12.06.2025 |
| Hour | 13:00 › 15:00 |
| Speaker |
Rouzbeh Pirayadi |
| Location | |
| Category | Conferences - Seminars |
EDIC candidacy exam
Exam president: Prof. Patrick Thiran
Thesis advisor: Prof. Paolo Ienne
Thesis co-advisor: Prof. Mirjana Stojilovic
Co-examiner: Prof. Thomas Bourgeat
Abstract
Unlike traditional high-level synthesis (HLS) approaches,
dataflow circuits use handshake signals to enable
dynamic scheduling, improving adaptability and performance.
We examine one proposed optimization that aims to reduce
latency and area by directly delivering tokens from producers
to consumers. However, such circuit transformations are applied
without formal correctness guarantees. To address this, we
explore the use of Kahn Process Networks for modeling and
reasoning about dataflow circuits, While Kahn networks offer
valuable insights, they are inadequate for capturing key features
of dataflow circuits. We then consider a more recent approach
that defines a mechanized operational semantics using two
equivalent intermediate representations (IRs). This framework
supports formal reasoning about properties such as parallelism
and establishes a foundation for verifying circuit correctness.
Nonetheless, its ability to fully express and reason about all circuit
behaviors remains an open question.
Selected papers
Exam president: Prof. Patrick Thiran
Thesis advisor: Prof. Paolo Ienne
Thesis co-advisor: Prof. Mirjana Stojilovic
Co-examiner: Prof. Thomas Bourgeat
Abstract
Unlike traditional high-level synthesis (HLS) approaches,
dataflow circuits use handshake signals to enable
dynamic scheduling, improving adaptability and performance.
We examine one proposed optimization that aims to reduce
latency and area by directly delivering tokens from producers
to consumers. However, such circuit transformations are applied
without formal correctness guarantees. To address this, we
explore the use of Kahn Process Networks for modeling and
reasoning about dataflow circuits, While Kahn networks offer
valuable insights, they are inadequate for capturing key features
of dataflow circuits. We then consider a more recent approach
that defines a mechanized operational semantics using two
equivalent intermediate representations (IRs). This framework
supports formal reasoning about properties such as parallelism
and establishes a foundation for verifying circuit correctness.
Nonetheless, its ability to fully express and reason about all circuit
behaviors remains an open question.
Selected papers
Practical information
- General public
- Free