Formal verification of integrated circuit hardware designs to implement integer division
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.
1. A computer-implemented method of verifying an integrated circuit hardware design to implement an integer divider, the integer divider configured to receive an input pair comprising a numerator N and a denominator D and output an output pair comprising a quotient q and a remainder r, the method comprising, in one or more processors:
verifying, for each non-negative input pair in a subset of non-negative input pairs, that an instantiation of the integrated circuit hardware design generates a correct output pair;
formally verifying, for each two non-negative input pairs that have one of one or more predetermined relationships, that an instantiation of the integrated circuit hardware design generates corresponding output pairs that have a predetermined relationship; and
outputting one or more signals indicating whether the verifications were successful.
2. The method of claim 1 , further comprising, in response to the one or more signals indicating that at least one verification was not successful, modifying the integrated circuit hardware design.
3. The method of claim 1 , further comprising, in response to the one or more signals indicating that the verifications were successful, manufacturing, at an integrated circuit manufacturing system, an integrated circuit according to the integrated circuit hardware design.
4. The method of claim 1 , wherein two non-negative input pairs comprises a first input pair comprising a numerator N and a denominator D and a second input pair comprising a numerator N′ and a denominator D′; and the two non-negative input pairs have one of the one or more predetermined relationships if D is the same as D′ and N has one of one or more predetermined relationships with N′.
5. The method of claim 4 , wherein the one or more predetermined relationships between N and N′ comprises N′=N+D.
6. The method of claim 4 , wherein the one or more predetermined relationships between N and N′ comprises N′=N+1.
7. The method of claim 4 , wherein the one or more predetermined relationships between N and N′ comprises N′=2 z N, 2 z N+1, 2 z N+2, . . . 2 z N+(2 z −1), wherein z is an integer.
8. The method of claim 7 , wherein z is equal to one.
9. The method of claim 8 , wherein the output pair corresponding to the first input pair comprises a quotient q and remainder r, and the output pair corresponding to the second input pair comprises a quotient q′ and a reminder r′ and:
if N′=2N and 2r<D then verifying that the corresponding output pairs have a predetermined relationship comprises verifying that r′=2r and q′=2q;
if N′=2N and 2r≥D then verifying that the corresponding output pairs have a predetermined relationship comprises verifying that r′=2r−D and q′=2q+1;
if N′=2N+1 and 2r<D then verifying that the corresponding output pairs have a predetermined relationship comprises verifying that r′=2r+1 and q′=2q; and
if N′=2N+1 and 2r>D then verifying that the corresponding output pairs have a predetermined relationship comprises verifying that r′=2r+1−D and q′=2q+1.
10. The method of claim 4 , wherein the one or more predetermined relationships between N and N′ comprises N′=αN, αN+1, αN+2, . . . αN+(α−1), wherein αis an integer.
11. The method of claim 7 , wherein the subset of non-negative input pairs comprises non-negative input pairs N,D where N=0.
12. The method of claim 11 , wherein verifying that an instantiation of the integrated circuit hardware design generates a correct output pair for a non-negative input pair comprises verifying that the output pair q,r satisfies q=0 and r=0.
13. The method of claim 1 , wherein the subset of non-negative input pairs comprises non-negative input pairs N,D where N<D.
14. The method of claim 13 , wherein verifying that an instantiation of the integrated circuit hardware design generates a correct output pair for a non-negative input pair comprises verifying that the output pair q,r satisfies q=0 and r=N.
15. The method of claim 1 , further comprising verifying, for each two input pairs comprising a non-negative input pair N,D and a negative input pair N′,D′ wherein N′=−N and/or D′=−D, that an instantiation of the hardware design generates corresponding output pairs that have a predetermined relationship.
16. The method of claim 15 , wherein the output pair corresponding to the non-negative input pair comprises a quotient q and a reminder r and the output pair corresponding to the negative input pair comprises a quotient q′ and a reminder r′; and
if N′=N and D′=−D, then verifying that the corresponding output pairs have a predetermined relationship comprises verifying that q′=−q and r′=r;
if N′=−N and D′=D, then verifying that the corresponding output pairs have a predetermined relationship comprises verifying that q′=−q and r′=−r; and
if N′=−N and D′=−D, then verifying that the corresponding output pairs have a predetermined relationship comprises verifying that q′=q and r′=−r.
17. The method of claim 15 , wherein the numerator N is represented in two's-complement format, and the method further comprises verifying, for each input pair wherein the numerator is the largest negative numerator representable in the two's-complement format, that an instantiation of the integrated circuit hardware design generates a correct output pair.
18. The method of claim 15 , wherein the denominator D is represented in two's-complement format, and the method further comprises verifying, for each input pair wherein the denominator is the largest negative denominator representable in the two's-complement format, that an instantiation of the integrated circuit hardware design generates a correct output pair.
19. A system to verify an integrated circuit hardware design to implement an integer divider, the integer divider configured to receive an input pair comprising a numerator N and a denominator D and output an output pair comprising 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, for each non-negative input pair in a subset of non-negative input pairs, that an instantiation of the integrated circuit hardware design generates a correct output pair,
formally verify, for each two non-negative input pairs that have one of one or more predetermined relationships, that an instantiation of the integrated circuit hardware design generates corresponding output pairs that have a predetermined relationship, and
output one or more signals indicating whether the verifications were successful.
20. 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, for each non-negative input pair in a subset of non-negative input pairs, that an instantiation of an integrated circuit hardware design to implement an integer divider generates a correct output pair, the integer divider configured to receive an input pair comprising a numerator N and a denominator D and output an output pair comprising a quotient q and a remainder r;
formally verify, for each two non-negative input pairs that have one of one or more predetermined relationships, that an instantiation of the integrated circuit hardware design generates corresponding output pairs that have a predetermined relationship; and
output one or more signals indicating whether the verifications were successful.