Functional Verification of Hardware Dividers using Algebraic Model

International audienceDivision is one of the most complex arithmetic operationsto implement and its hardware implementation requires athorough verification on the gate level. Dividers circuits are difficultto prove using standard Boolean verification methods, such asequivalence checking and SAT, as they require "bit-blasting" ontobit-level netlists. Other verification approaches, such as theoremprovers, concentrate mostly on proving the correctness of thedivision algorithm and the resulting architectures. However, theverification of low-level hardware implementation of dividershas received only a limited attention. This paper addresses theproblem of formally verifying gate-level divider circuits using analgebraic model. In contrast to standard approaches using SATor equivalence checking, our method verifies whether the gateleveldivider circuit actually performs a division, without a needfor a reference design. The method extends algebraic rewritingtechnique, successfully used to prove other arithmetic circuits, todividers