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

Patent metadata

Field	Value
Publication number	US-12197835-B2
Application number	US-202318369338-A
Country	US
Kind code	B2
Filing date	Sep 18, 2023
Priority date	Apr 15, 2019
Publication date	Jan 14, 2025
Grant date	Jan 14, 2025

Abstract

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.

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 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

Assignees

• Imagination Tech Ltd

Inventors

• Elliott Sam
• Mckemey Robert
• Freiburghaus Max

Classifications

• G06F2119/16

  Equivalence checking · CPC title

• G06F30/3308

  using simulation · CPC title

• G06F30/3323 Primary

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

• G06F30/33 Primary

  Design verification, e.g. functional simulation or model checking · CPC title