Translating back and forth between braided and lattice surgery surface code circuits

High-level surface code circuits are implemented, for example, by lattice surgery (LS) or braiding. Such circuits are compiled by starting from a quantum circuit diagram, and the resulting LS or braided diagrams are considered to be different representations of the initial circuit. Herein, we present a systematic method to translate between and LS and braided diagrams. Our translation method is based on quantum circuit identities, and we use the ZX calculus to verify the translation. Our method can be used for the automatic compilation, the symbolic verification (ie. check that the surface code circuits are compiled correctly) and the benchmarking (ie. compute how many physical qubits and how long it takes to execute the circuit) of high-level surface code circuits. We expect for our method to be an integral part of the next generation quantum circuit compilers.