BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Formal Reasoning on Dataflow Circuits
DTSTART:20250612T130000
DTEND:20250612T150000
DTSTAMP:20260502T045855Z
UID:a3e4f6ebbc6de5b5ee31ad74fb0b5743753f780c20b95e79342880dc
CATEGORIES:Conferences - Seminars
DESCRIPTION:\nRouzbeh Pirayadi \nEDIC candidacy exam\nExam president: Pro
 f. Patrick Thiran\nThesis advisor: Prof. Paolo Ienne\nThesis co-advisor: P
 rof. Mirjana Stojilovic\nCo-examiner: Prof. Thomas Bourgeat\n\nAbstract\nU
 nlike traditional high-level synthesis (HLS) approaches\,\ndataflow circui
 ts use handshake signals to enable\ndynamic scheduling\, improving adaptab
 ility and performance.\nWe examine one proposed optimization that aims to 
 reduce\nlatency and area by directly delivering tokens from producers\nto 
 consumers. However\, such circuit transformations are applied\nwithout for
 mal correctness guarantees. To address this\, we\nexplore the use of Kahn 
 Process Networks for modeling and\nreasoning about dataflow circuits\, Whi
 le Kahn networks offer\nvaluable insights\, they are inadequate for captur
 ing key features\nof dataflow circuits. We then consider a more recent app
 roach\nthat defines a mechanized operational semantics using two\nequivale
 nt intermediate representations (IRs). This framework\nsupports formal rea
 soning about properties such as parallelism\nand establishes a foundation 
 for verifying circuit correctness.\nNonetheless\, its ability to fully exp
 ress and reason about all circuit\nbehaviors remains an open question.\n\n
 Selected papers\n\n	Unleashing Parallelism in Elastic Circuits with Faster
  Token Delivery Link\n	 The Semantics of a Simple Language for Parallel P
 rogramming Link\n	A Mechanized Semantics for Dataflow Circuits Link\n
LOCATION:BC 333 https://plan.epfl.ch/?room==BC%20333
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR