  Seminal work by Cortadella, Kondratyev, Lavagno, and Sotiriou includes a
hand-written proof that a particular handshaking protocol preserves flow
equivalence, a notion of equivalence between synchronous latch-based
specifications and their desynchronized bundled-data asynchronous
implementations. In this work we identify a counterexample to Cortadella et
al.'s proof illustrating how their protocol can in fact lead to a violation of
flow equivalence. However, two of the less concurrent protocols identified in
their paper do preserve flow equivalence. To verify this fact, we formalize
flow equivalence in the Coq proof assistant and provide mechanized,
machine-checkable proofs of our results.
