Formal verification of integrated circuit hardware designs to implement integer division

A system to verify an integrated circuit hardware design to implement an integer divider, the integer divider configured to receive a numerator N and a denominator D and output a quotient q and a remainder r, the system comprising:

• one or more processors;
• and
• memory, comprising:
• a formal verification tool;
• computer-readable instructions that when executed by the one or more processors cause the one or more processors to:
• verify a base property of the integrated circuit hardware design, wherein verifying the base property verifies 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;
• formally verify, by the formal verification tool, one or more range reduction properties of the integrated circuit hardware design, wherein verifying the one or more range reduction properties verifies 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 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;
• and
• output one or more signals indicating whether the properties have been successfully verified.

A non-transitory computer readable storage medium having stored thereon computer readable instructions that, when executed at a computer system, cause the computer system to:

• verify a base property of an integrated circuit hardware design to implement an integer divider, the integer divider configured to receive a numerator N and a denominator D and output a quotient q and a remainder r, wherein verifying the base property verifies 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;
• formally verify, by a formal verification tool, one or more range reduction properties of the integrated circuit hardware design, wherein verifying the one or more range reduction properties verifies 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 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;
• and
• output one or more signals indicating whether the properties have been successfully verified.