Dataflow circuits have become important targets for high-level synthesis (HLS) compilers, which generate circuits from high-level programs and provide an effective approach to circuit programming. A major challenge for HLS compilers is the optimization of the automatically generated circuits. Recent work implemented algorithms which search for common patterns and replace complex parts with smaller and simpler components.

To ensure that optimized circuits remain functionally equivalent to their originals, equivalence checking is needed. As dataflow circuits exhibit asynchronous behavior and depend on timings of inputs and outputs, it is insufficient to use standard sequential equivalence verification strategies. The current method depends on inserting both circuits into a larger framework with user-defined auxiliary circuits and buffers controlling timing and at the end checking properties of the resulting combined circuit. This leads to a significant overhead.

This thesis proposes the use of weak-trace equivalence to guide optimization and to integrate existing verification tools to provide formal guarantees. With these tools we reduce the time and complexity compared to the existing method. We integrate them into the existing synthesis pipeline and enable future integration of other tools for sound optimization of dataflow circuits.