Verification of hardware design for an integrated circuit that implements a function that is polynomial in one or more sub-functions

Abstract

Methods and systems for verifying a hardware design for an integrated circuit that implements a function that is polynomial of degree k in a sub-function p over a set of values of p, k being an integer greater than or equal to one. The methods include: verifying that an instantiation of the hardware design correctly evaluates the sub-function p; formally verifying that an instantiation of the hardware design implements a function that is polynomial of degree k in p by formally verifying that, for all values of p in the set of values of p, an 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 e different values of p in the set of values of p, 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.

What is claimed is: 
     
       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 a sub-function p over a set of values of p, k being an integer greater than or equal to one, the method comprising, in one or more processors:
 verifying that an instantiation of the hardware design correctly evaluates the sub-function p; 
 formally verifying that an instantiation of the hardware design implements a function that is polynomial of degree k in p by formally verifying that, for all values of p in the set of values of p, an 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 e different values of p in the set of values of p, 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 when k is one, formally verifying that, for all p in the set of values of p, an instantiation of the hardware design has a constant k th  difference comprises formally verifying that a difference in outputs of an instantiation of the hardware design for any two consecutive values of p in the set of values of p is constant. 
     
     
       3. The method of  claim 1 , wherein the sub-function comprises one or more input variables, and formally verifying that for all values of p in the set of values of p an instantiation of the hardware design has a constant k th  difference comprises, during the formal verification, identifying values of the one or more input variables that result in consecutive values of p in the set of values of p, and comparing outputs of an instantiation of the hardware design in response to values of the one or more input variables that result in consecutive values of p in the set of values of p. 
     
     
       4. The method of  claim 3 , wherein identifying values of the one or more input variables that result in consecutive values of p in the set of values of p comprises:
 determining a first output of an instantiation of the hardware design constrained to evaluate the sub-function; 
 determining a second output of an instantiation of the hardware design constrained to evaluate the sub-function and the second output is constrained to be greater than the first output by a predetermined number; and 
 identifying the values of the one or more input variables of the sub-function used to generate the first output and the values of the one or more input variables of the sub-function used to generate the second output as values of the one or more input variables that result in consecutive values of p in the set of values of p. 
 
     
     
       5. The method of  claim 4 , wherein comparing outputs of an instantiation of the hardware design in response to values of the one or more input variables that result in consecutive values of p in the set of values of p comprises:
 determining a third output of an instantiation of the hardware design when the values of the one or more input variables match the values of the one or more input variables used to generate the first output; 
 determining a fourth output of an instantiation of the hardware design when the values of the one or more input variables match the values of the one or more input variables used to generate the second output and the values of any other input variables to the function match the values of those other input variables used to generate the third output; and 
 comparing the third output and the fourth output. 
 
     
     
       6. 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 e different values of p in the set of values of p comprises verifying that an instantiation of the hardware design generates a correct output in response to each of at least e different values of p in the set of values of p according to the function. 
     
     
       7. The method of  claim 1 , wherein the function is also polynomial of degree r in p over a second set of values of p and the method further comprises:
 formally verifying that an instantiation of the hardware design implements a function that is polynomial of degree r in p by formally verifying that for all p in the second set of values of p an 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 p in the second set of values of p. 
 
     
     
       8. The method of  claim 1 , wherein:
 the function is also polynomial of degree q in a second sub-function z over a set of values of z; 
 the method further comprising:
 verifying that an instantiation of the hardware design correctly evaluates the second sub-function z; and 
 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 an 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 e different values of p in the set of values of p is performed for at least q different values of z. 
 
     
     
       9. The method of  claim 8 , wherein the sub-function p and the second sub-function z are ordered and the verification that an instantiation of the hardware design has a constant difference for the lower ordered sub-function is performed under a constraint that the higher ordered sub-function is restricted to at least k or at least q values of that sub-function. 
     
     
       10. The method of  claim 1 , wherein:
 the sub-function has one or more input variables, and the function has at least one additional input variable; 
 the formal verification that for all values of p in the set of values of p 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 e different values of p in the set of values of p is performed for each valid value of each of the at least one additional input variable. 
 
     
     
       11. The method of  claim 1 , wherein an output of the sub-function p is a multiple bit binary number and formally verifying that for all values of p in the set of values of p 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 sub-function output. 
     
     
       12. The method of  claim 1 , wherein:
 an output of the sub-function p is a multiple bit binary number; 
 k is equal to one; 
 the constant k th  difference is c; and further comprising 
 verifying that an instantiation of the hardware design has a constant k th  difference comprises verifying for each bit i of the output of the sub-function p that the difference in the outputs of an instantiation of the hardware design in response to a first value of p and a second value of p is equal to 2 i *c wherein the i th  least significant bit of the first value of p is one and the i th  least significant bit of the second value of p is zero and all other bits of the first value of p and the second value of p are the same. 
 
     
     
       13. The method of  claim 12 , wherein the bits of the output of the sub-function p are ordered and the verification for a particular bit of the output of the sub-function p is performed under a constraint that any bit higher in the order than the particular bit is zero for the first and second values of p. 
     
     
       14. The method of  claim 12 , wherein the function is a dot product such that the function comprises a sum of a plurality of products, and the sub-function p is one of the plurality of products, and the method further comprises formally verifying that an instantiation of the hardware design is permutation independent with respect to the products. 
     
     
       15. The method of  claim 14 , wherein:
 the bits of the output of the sub-function p are ordered; and 
 the verification of the constant k th  difference for a particular bit of the output of the sub-function p is performed under a constraint that any bit higher in the order than the particular bit is zero for outputs of the other products. 
 
     
     
       16. The method of  claim 1 , further comprising, in response to determining that at least one of the verifications 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 verifications were successful, manufacturing, using an integrated circuit manufacturing system, the integrated circuit according to the hardware design. 
     
     
       18. The method of  claim 1 , wherein the set of values of p comprise equally spaced values of p. 
     
     
       19. A system for verifying a hardware design for an integrated circuit that implements a function that is polynomial of degree k in a sub-function p for a set of values of p, 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:
 verify, using the one or more verification tools, that an instantiation of the hardware design correctly evaluates the sub-function p; 
 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 p by formally verifying that, for all values of p in the set of values of p, an instantiation of the hardware design has a constant k th  difference; and 
 verify, using the one or more verification tools, that an instantiation of the hardware design generates an expected output in response to each of at least e different values of p in the set of values of p, 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. 
 
 
     
     
       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 .