Verification of hardware design for integrated circuit implementing polynomial input variable function
Methods and systems for verifying a hardware design for an integrated circuit that implements a function that is polynomial in an input variable x over a set of values of x. The method includes 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 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 k different values of x in the set of values of x.
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 an 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 instantiation of the hardware design has a constant k th difference; and
verifying that an instantiation of the hardware design generates an expected output in response to each of at least k different values of x in the set of values of x.
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 an instantiation of the hardware design has a constant k th difference comprises formally verifying that the 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 values of x in the set of values of x an instantiation of the hardware design has a constant k th difference comprises formally verifying that a difference in outputs of the instantiation of the hardware design 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 an instantiation of the hardware design generates an expected output in response to each of at least k different values of x in the set of values of x comprises verifying that the instantiation of the hardware design generates a correct output according to the function in response to each of at least k different values of x in the set of values of x.
5. The method of claim 1 , wherein verifying that an instantiation of the hardware design generates an expected output in response to each of at least k different values of x in the set of values of x comprises verifying a functional equivalence of the instantiation of the hardware design and an instantiation of another hardware design for at least k 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
further comprising formally verifying that for all values of 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 instantiation of the hardware design and the instantiation of the other hardware design for at least k different values of x in the set of values of x comprises verifying that for each of the at least k different values of x in the set of values of x the 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, the method further comprising:
formally verifying that an instantiation of the hardware design implements a function that is polynomial of degree r in x by formally verifying that for all values of x in the second set of values of x the instantiation of the hardware design has a constant r th difference; and
verifying that an 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 of degree q in a second input variable z over a set of values of z;
the method further comprising formally verifying that an 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 instantiation of the hardware design has a constant q th difference; and
the verification that an instantiation of the hardware design generates an expected output in response to each of at least k 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 an 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 an instantiation of the hardware design generates an expected output in response to each of at least k 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 an 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 an instantiation of the hardware design has a constant k th difference comprises verifying for each bit i of the input variable x that the difference in the outputs of the 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 an 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 values of x in the set of values of x an instantiation of the hardware design has a constant k th difference comprises formally verifying that for all values of x in the set of values of x the 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 was successful and the verification was successful, manufacturing, using an integrated circuit manufacturing system, the integrated circuit according to the hardware design.
18. The method of claim 1 , wherein when a value of the k th difference is predetermined the expected output of an instantiation of the hardware design is verified for each of at least k different values of x in the set of values of x; and when the value of the k th difference is not predetermined the expected output of an instantiation of the hardware design is verified for at least k+1 different values of x in the set of values of x.
19. 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 an 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 instantiation of the hardware design has a constant k th difference; and
verify, using one of the one or more verification tools, that an instantiation of the hardware design generates an expected output in response to each of at least k different values of x in the set of values of x.
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 perform the method as set forth in claim 1 .