Verification of hardware design for integrated circuit implementing polynomial input variable function

1. A computer-implemented method of verifying a hardware design for an integrated circuit that implements a function that is polynomial of degree k in an input variable x over a set of values of x, the set of values of x comprising equally spaced values of x, k being an integer greater than or equal to one, the method comprising in one or more processors:

formally verifying that a first instantiation of the hardware design implements a function that is polynomial of degree k in x by formally verifying that for all values of x in the set of values of x the first instantiation of the hardware design has a constant k th difference; and

verifying that a second instantiation of the hardware design generates an expected output in response to each of at least e different values of x in the set of values of x, wherein e is equal to k when a value of the k th difference is predetermined and e is equal to k+1 when the value of the k th difference is not predetermined.

2. The method of claim 1 , wherein the set of values of x comprises a contiguous block of integers, and formally verifying that for all values of x in the set of values of x the first instantiation of the hardware design has a constant k th difference comprises formally verifying that the first instantiation of the hardware design P satisfies:

∑

i

=

0

k

⁢

(

k

i

)

⁢

(

-

1

)

i

⁢

P

⁡

(

x

+

i

)

=

c

for all values of x in the set of values of x wherein c is a constant.

3. The method of claim 1 , wherein when k is one, formally verifying that for all x in the set of values of x the first instantiation of the hardware design has a constant k th difference comprises formally verifying that a difference in outputs of the first instantiation in response to any two consecutive values of x in the set of values of x is constant.

4. The method of claim 1 , wherein verifying that the second instantiation of the hardware design generates an expected output in response to each of at least e different values of x in the set of values of x comprises verifying that the second instantiation of the hardware design generates a correct output in response to each of at least e different values of x in the set of values of x according to the function.

5. The method of claim 1 , wherein verifying that the second instantiation of the hardware design generates an expected output in response to each of at least e different values of x in the set of values of x comprises verifying a functional equivalence of the second instantiation of the hardware design and an instantiation of another hardware design for at least e different values of x in the set of values of x wherein the other hardware design is for an integrated circuit that implements a function that is polynomial of degree k in x for all x in the set of values of x; and

the method further comprises formally verifying that for all x in the set of values of x the instantiation of the other hardware design has a constant k th difference.

6. The method of claim 5 , wherein verifying the functional equivalence of the second instantiation of the hardware design and the instantiation of the other hardware design for at least e different values of x in the set of values of x comprises verifying that for each of the at least e different values of x in the set of values of x the second instantiation of the hardware design and the instantiation of the other hardware design generate a same output as each other.

7. The method of claim 1 , wherein the function is also polynomial of degree r in x over a second set of values of x and the method further comprises:

formally verifying that a third instantiation of the hardware design implements a function that is polynomial of degree r in x by formally verifying that for all x in the second set of values of x the third instantiation of the hardware design has a constant r th difference; and

verifying that a fourth instantiation of the hardware design generates an expected output in response to each of r+1 different values of x in the second set of values of x.

8. The method of claim 1 , wherein:

the function is also polynomial in a second input variable z over a set of values of z;

the method further comprises formally verifying that a fifth instantiation of the hardware design implements a function that is polynomial of degree q in z by formally verifying that for all values of z in the set of values of z the fifth instantiation of the hardware design has a constant q th difference; and

the verification that the second instantiation of the hardware design generates an expected output in response to each of at least e different values of x in the set of values of x is performed for at least q different values of z.

9. The method of claim 8 , wherein the input variable x and the second input variable z are ordered and the verification that an instantiation of the hardware design has a constant difference for the lower ordered input variable is performed under a constraint that the higher ordered input variable is restricted to at least k or at least q values of that input variable.

10. The method of claim 1 , wherein:

the function has at least one additional input variable;

the formal verification that for all values of x in the set of values of x the first instantiation of the hardware design has a constant k th difference is performed for each valid value of each of the at least one additional input variable; and

the verification that the second instantiation of the hardware design generates an expected output in response to each of at least e different values of x in the set of values of x is performed for each valid value of each of the at least one additional input variable.

11. The method of claim 1 , wherein the input variable x is a multiple bit binary number and formally verifying that for all values of x in the set of values of x the first instantiation of the hardware design has a constant k th difference comprises verifying the constant k th difference separately for each bit of the input variable x.

12. The method of claim 1 , wherein:

the input variable x is a multiple bit binary number;

k is equal to one;

the constant k th difference is c; and

verifying that the first instantiation of the hardware design has a constant k th difference comprises verifying for each bit of the input variable x that the difference in the outputs of the first instantiation of the hardware design in response to a first value of x and a second value of x is equal to 2 i *c wherein the i th least significant bit of the first value of x is one and the i th least significant bit of the second value of x is zero and all other bits of the first value of x and the second value of x are the same.

13. The method of claim 1 , wherein the function is a dot product of a first input vector comprising a plurality of elements and a second input vector comprising a plurality of elements and the input variable x is one of the elements of one of the first input vector and the second input vector and the method further comprises formally verifying that a sixth instantiation of the hardware design is permutation independent with respect to the elements of the first and second input vectors.

14. The method of claim 1 , wherein the function is polynomial mod N in the input variable x and formally verifying that for all x in the set of values of x the first instantiation of the hardware design has a constant k th difference comprises formally verifying that for all x in the set of values of x the first instantiation of the hardware design has a constant k th difference mod N, wherein N is an integer greater than 1.

15. The method of claim 1 , further comprising outputting one or more signals indicating whether the formal verification and/or the verification was successful.

16. The method of claim 1 , further comprising, in response to determining that the formal verification or the verification was not successful, modifying the hardware design to generate a modified hardware design.

17. The method of claim 1 , further comprising, in response to determining that the formal verification and the verification was successful, manufacturing, using an integrated circuit manufacturing system, the integrated circuit according to the hardware design.

18. A system for verifying a hardware design for an integrated circuit that implements a function that is polynomial of degree k in an input variable x over a set of values of x, the set of values of x comprising equally spaced values of x, k being an integer greater than or equal to one, the system comprising:

memory configured to store:

the hardware design, and

one or more verification tools comprising at least one formal verification tool; and

one or more processors configured to:

formally verify, using the at least one formal verification tool, that a first instantiation of the hardware design implements a function that is polynomial of degree k in x by formally verifying that for all x in the set of values of x the first instantiation of the hardware design has a constant k th difference, and

verify, using one of the one or more verification tools, that a second instantiation of the hardware design generates an expected output in response to each of at least e different values of x in the set of values of x, wherein e is equal to k when a value of the k th difference is predetermined and e is equal to k+1 when the value of the k th difference is not predetermined.

19. 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 perform the method as set forth in claim 1 .