Verification of hardware design for component that evaluates an algebraic expression using decomposition and recombination

Patent metadata

Field	Value
Publication number	US-11829694-B2
Application number	US-202218076338-A
Country	US
Kind code	B2
Filing date	Dec 6, 2022
Priority date	Oct 14, 2020
Publication date	Nov 28, 2023
Grant date	Nov 28, 2023

Abstract

A hardware design for a component that evaluates a main algebraic expression comprising at least two variables is verified, the main algebraic expression being representable as a lossless combination of a plurality of sub-algebraic expressions, and one or more of the at least two variables can be constrained to cause an instantiation of the hardware design to evaluate each of the sub-algebraic expressions. An instantiation of the hardware design is verified as correctly evaluating each of the plurality of sub-algebraic expressions, and the instantiation of the hardware design is formally evaluated as correctly evaluating one or more combinations of sub-algebraic expressions, wherein the one or more combinations comprises a combination that is equivalent to the main algebraic expression.

First claim

What is claimed is:

1. A computer-implemented method of verifying a hardware design for a component that evaluates a main algebraic expression comprising at least two variables, the main algebraic expression being representable as a lossless combination of a plurality of sub-algebraic expressions, and one or more of the at least two variables can be constrained to cause an instantiation of the hardware design to evaluate each of the sub-algebraic expressions, the method comprising, at one or more processors:
verifying that an instantiation of the hardware design correctly evaluates each of the plurality of sub-algebraic expressions; and
formally verifying that an instantiation of the hardware design correctly evaluates one or more combinations of sub-algebraic expressions, wherein the one or more combinations comprises a combination that is equivalent to the main algebraic expression.

2. The method of claim 1 , wherein formally verifying that an instantiation of the hardware design correctly evaluates a combination of the one or more combinations comprises comparing instantiations of the hardware design under different constraints.

3. The method of claim 1 , wherein the formal verification that an instantiation of the hardware design correctly evaluates a combination of the one or more combinations is based on an instantiation of the hardware design constrained to evaluate the combination and an instantiation of the hardware design constrained to evaluate a sub-algebraic expression or another combination of the one or more combinations.

4. The method of claim 1 , wherein verifying that an instantiation of the hardware design correctly evaluates a certain sub-algebraic expression of the plurality of sub-algebraic expressions comprises, for each valid value of each variable in the certain sub-algebraic expression:
determining a first output of an instantiation of the hardware design constrained to evaluate the certain sub-algebraic expression;
determining a second output of a high-level model of the hardware design constrained to evaluate the certain sub-algebraic expression and constrained to use the same values for the variables of the certain sub-algebraic expression that were used to generate the first output; and
verifying that the first output matches the second output.

5. The method of claim 1 , wherein a specific sub-algebraic expression of the plurality of sub-algebraic expressions is polynomial of degree k in a variable x for all values of x in a set of values of x, and verifying that an instantiation of the hardware design correctly evaluates the specific sub-algebraic expression comprises:
formally verifying that an instantiation of the hardware design constrained to evaluate the specific sub-algebraic expression implements an expression that is polynomial of degree k in x by 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; and
verifying that an instantiation of the hardware design constrained to evaluate the specific sub-algebraic expression 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.

6. The method of claim 1 , wherein the main algebraic expression is permutation invariant with respect to a particular sub-algebraic expression and a particular algebraic expression that is verified in the method, and verifying that an instantiation of the hardware design correctly evaluates the particular sub-algebraic expression comprises, for all valid values of the variables of the particular algebraic expression:
determining a first output of an instantiation of the hardware design constrained to evaluate the particular algebraic expression;
determining a second output of an instantiation of the hardware design constrained to evaluate the particular sub-algebraic expression when the values of the variables of the particular sub-algebraic expression are the same as the values of the variables of the particular algebraic expression used to generate the first output; and
verifying that the first output matches the second output.

7. The method of claim 1 , wherein each combination of the one or more combinations is a combination of a first algebraic expression and a second algebraic expression, and each of the first and second algebraic expressions is one of: a sub-algebraic expression and another combination of the one or more combinations.

8. The method of claim 7 , wherein formally verifying that an instantiation of the hardware design correctly evaluates a specific combination of the one or more combinations comprises, for valid values of each variable of the first algebraic expression and the second algebraic expression of the specific combination:
determining a first output of an instantiation of the hardware design constrained to evaluate the first algebraic expression;
determining a second output of an instantiation of the hardware design constrained to evaluate the second algebraic expression;
determining a third output of an instantiation of the hardware design constrained to evaluate the specific combination, wherein the variables of the first algebraic expression have the same values as the variables of the first algebraic expression used to generate the first output, and the variables of the second algebraic expression have the same values as the variables of the second algebraic expression used to generate the second output; and
verifying that the third output matches the combination of the first and second outputs.

9. The method of claim 7 , wherein a particular combination of the one or more combinations combines the first algebraic expression and the second algebraic expression through an addition operation, and formally verifying that an instantiation of the hardware design correctly evaluates the particular combination comprises:
formally verifying that an instantiation of the hardware design constrained to evaluate the particular combination implements an expression that is polynomial of degree k in the first algebraic expression by formally verifying that, for all values of the first algebraic expression, an instantiation of the hardware design constrained to evaluate the particular combination has a constant k th difference; and
verifying that an instantiation of the hardware design constrained to evaluate the particular combination generates an expected output in response to each of at least e different values of the first algebraic expression, 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.

10. The method of claim 9 , wherein formally verifying that, for all values of the first algebraic expression, an instantiation of the hardware design constrained to evaluate the particular combination has a constant k th difference comprises, during the formal verification, identifying values of the variables of the first algebraic expression that result in consecutive values of the first algebraic expression, and comparing outputs of an instantiation of the hardware design constrained to evaluate the particular combination in response to values of the variables of the first algebraic expression that result in consecutive values of the first algebraic expression.

11. The method of claim 10 , wherein identifying values of the variables of the first algebraic expression that result in consecutive values of the first algebraic expression comprises:
determinin

Assignees

• Imagination Tech Ltd

Inventors

• Elliott Sam
• Edmonds Rachel

Classifications

• G06F30/3323 Primary

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

• G06F30/392

  Floor-planning or layout, e.g. partitioning or placement · CPC title

• G06F2111/04

  Constraint-based CAD · CPC title

• G06F30/33 Primary

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

• G06F2115/02

  System on chip [SoC] design · CPC title