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

Patent metadata

Field	Value
Publication number	US-12190035-B2
Application number	US-202117501666-A
Country	US
Kind code	B2
Filing date	Oct 14, 2021
Priority date	Apr 15, 2019
Publication date	Jan 7, 2025
Grant date	Jan 7, 2025

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.

First claim

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

Assignees

• Imagination Tech Ltd

Inventors

• Edmonds Rachel
• Elliott Sam

Classifications

• G06F2119/16

  Equivalence checking · CPC title

• G06F30/3323 Primary

  using formal methods, e.g. equivalence checking or property checking · CPC title