In recent years, the use of Symbolic Computer Algebra (SCA) has enabled a huge progress in the formal verification of arithmetic circuits. Several different approaches have been proposed showing great success especially for the verification of integer multipliers, but more recently also for the verification of integer dividers. The goal of this paper is to provide a comprehensive review of the current state of the art in arithmetic circuit verification using SCA, starting with a careful review of the underlying theory, through the identification of main challenges in arithmetic circuit verification, an overview of numerous non-trivial optimization methods, to an experimental evaluation of SCA-based verification.