SPEAR: Hardware-based Implicit Rewriting for Square-root Circuit Verification

The paper addresses formal verification of gate-level square-root circuits. Division and square root functions are all tied to the basic Intel architecture and proving the correctness of their hardware implementation is of great importance. In contrast to standard approaches that use SAT or equivalence checking, our method verifies whether the gate-level square-root circuit actually performs a root operation, instead of checking equivalence with a reference design. The method extends the algebraic rewriting technique developed earlier for multipliers and significantly improves its efficiency by introducing the concept of hardware-based rewriting. The tool called SPEAR, developed in this work enables the verification of a 256-bit gatelevel square-root circuit with 0.26 million gates in under 18 minutes.