  We define a formal framework for equivalence checking of sequential quantum
circuits. The model we adopt is a quantum state machine, which is a natural
quantum generalisation of Mealy machines. A major difficulty in checking
quantum circuits (but not present in checking classical circuits) is that the
state spaces of quantum circuits are continuums. This difficulty is resolved by
our main theorem showing that equivalence checking of two quantum Mealy
machines can be done with input sequences that are taken from some chosen basis
(which are finite) and have a length quadratic in the dimensions of the state
Hilbert spaces of the machines. Based on this theoretical result, we develop an
(and to the best of our knowledge, the first) algorithm for checking
equivalence of sequential quantum circuits with running time
$\mathcal{O}(2^{3m+5l}(2^{3m}+2^{3l}))$, where $m$ and $l$ denote the numbers
of input and internal qubits, respectively. The complexity of our algorithm is
comparable with that of the known algorithms for checking classical sequential
circuits in the sense that both are exponential in the number of (qu)bits.
Several case studies and experiments are presented.
