  Coarse-grained reconfigurable arrays (CGRAs) have gained attention in recent
years due to their promising power efficiency compared to traditional von
Neumann architectures. To program these architectures using ordinary languages
such as C, a dataflow compiler must transform the original sequential,
imperative program into an equivalent dataflow graph, composed of dataflow
operators running in parallel. This transformation is challenging since the
asynchronous nature of dataflow graphs allows out-of-order execution of
operators, leading to behaviors not present in the original imperative
programs.
  We address this challenge by developing a translation validation technique
for dataflow compilers to ensure that the dataflow program has the same
behavior as the original imperative program on all possible inputs and
schedules of execution. We apply this method to a state-of-the-art dataflow
compiler targeting the RipTide CGRA architecture. Our tool uncovers 8 compiler
bugs where the compiler outputs incorrect dataflow graphs, including a data
race that is otherwise hard to discover via testing. After repairing these
bugs, our tool verifies the correct compilation of all programs in the RipTide
benchmark suite.
