Formal verification of integrated circuit hardware designs to implement integer division

Abstract

Computer-implemented methods of verifying an integrated circuit hardware design to implement an integer divider wherein the integer divider is configured to receive a numerator N and a denominator D and output a quotient q and a remainder r. The method includes (a) verifying a base property is true for the integrated circuit hardware design and (b) formally verifying that one or more range reduction properties are true for the integrated circuit hardware design. The base property is configured to verify that an instantiation of the integrated circuit hardware design will generate a correct output pair q,r in response to any input pair N,D in a subset of non-negative input pairs. The one or more range reduction properties are configured to verify that if an instantiation of the integrated circuit hardware design will generate an output pair q,r in response to a non-negative input pair N,D then an instantiation of the integrated circuit hardware design to implement the integer divider will generate an output pair q',r′ that has a predetermined relationship with q and r in response to another non-negative input pair N′,D where N and N′ have one of one or more predetermined relationships.