The paper addresses formal verification of gate-levelsquare-root circuits. Division and square root functions are alltied to the basic Intel architecture and proving the correctnessof their hardware implementation is of great importance. Incontrast to standard approaches that use SAT or equivalencechecking, our method verifies whether the gate-level square-rootcircuit actually performs a root operation, instead of checkingequivalence with a reference design. The method extends thealgebraic rewriting technique developed earlier for multipliersand significantly improves its efficiency by introducing theconcept of hardware-based rewriting. The tool called SPEAR,developed in this work enables the verification of a 256-bit gatelevelsquare-root circuit with 0.26 million gates in under 18minutes.