  Despite the rapid development of quantum computing these years,
state-of-the-art quantum devices still contain only a very limited number of
qubits. One possible way to execute more realistic algorithms in near-term
quantum devices is to employ dynamic quantum circuits, in which measurements
can happen during the circuit and their outcomes are used to control other
parts of the circuit. This technique can help to significantly reduce the
resources required to achieve a given accuracy of a quantum algorithm. However,
since this type of quantum circuits are more flexible, their verification is
much more challenging. In this paper, we give a formal definition of dynamic
quantum circuits and then propose to characterise their functionality in terms
of ensembles of linear operators. Based on this novel semantics, two dynamic
quantum circuits are equivalent if they have the same functionality. We further
propose and implement two decision diagram-based algorithms for checking the
equivalence of dynamic quantum circuits. Experiments show that embedding
classical logic into conventional quantum circuits does not incur significant
time and space burden.
