SPEAR: Hardware-based Implicit Rewriting for Square-root Circuit Verification
Atif Yasin1,a, Tiankai Su1,b, Sébastien Pillement2,c and Maciej Ciesielski2,d
1University of Massachusetts, Amherst, MA, USA
aayasin@umass.edu
btiankaisu@umass.edu
2Univ Nantes, CNRS, IETR UMR 6164, F-44000 Nantes, France
csebastien.pillement@univ-nantes.fr
dciesiel@umass.edu
ABSTRACT
The paper addresses the formal verification of gatelevel square-root circuits. Division and square root functions are some of the most complex arithmetic operations to implement and proving the correctness of their hardware implementation is of great importance. In contrast to standard approaches that use satisfiability and equivalence checking techniques, the presented 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 introduces a novel technique of implicit hardware rewriting. The tool called SPEAR based on hardware rewriting enables the verification of a 256-bit gate-level square-root circuit with 0.26 million gates in under 18 minutes.
