Abstract
We present a method for reasoning about the synchronization behavior of reshuffled handshaking expansions. The technique introduced converts the handshaking expansion into communicating hardware processes. We identify and discuss some of the limitations of the method. We show how the approach can be applied to analyze both the performance and the correctness of handshaking expansions.