Verification of hardware designs to implement floating point power functions

Patent metadata

Field	Value
Publication number	US-10229236-B2
Application number	US-201715492205-A
Country	US
Kind code	B2
Filing date	Apr 20, 2017
Priority date	Apr 27, 2016
Publication date	Mar 12, 2019
Grant date	Mar 12, 2019

Abstract

A method of exhaustively verifying a property of a hardware design to implement a floating point power function. The method includes, formally verifying that the hardware design is recurrent over sets of β input exponents, wherein β is an integer that is a multiple of the reciprocal of the exponent of the power function; and for each recurrent input range of the hardware design, exhaustively simulating the hardware design over a simulation range to verify the property is true over the simulation range, wherein the simulation range comprises only β input exponents.

First claim

The invention claimed is:

1. A computer-implemented method of exhaustively verifying a property of a hardware design to implement a floating point power function defined by an exponent, the hardware design being configured to, in response to receiving a floating point input that has an input mantissa and an input exponent, produce a corresponding floating point output that has an output mantissa and an output exponent, the method comprising, in one or more processors:
formally verifying, using one or more formal assertions, that the hardware design is recurrent over sets of β input exponents, the hardware design being recurrent over sets of β input exponents if for any two non-exception floating point inputs in a recurrent input range that have the same input mantissa and have input exponents X and Y that are related by an integer multiple of β the corresponding floating point outputs produced by the hardware design have the same output mantissa and have output exponents X′ and Y′ that satisfy the equation X′−t·X=Y′−t·Y, wherein t is the exponent of the floating point power function and β is an integer that is a multiple of 1/t; and
for each recurrent input range of the hardware design, exhaustively simulating the hardware design over a simulation range to verify the property over the simulation range, wherein the simulation range comprises floating point inputs based on a set of β input exponents in the recurrent input range.

2. The method of claim 1 , wherein the set of β input exponents comprises an input exponent from each of a plurality of exponent classes, each exponent class comprising input exponents with a same value modulo β.

3. The method of claim 1 , wherein the hardware design has a single recurrent input range that comprises positive and negative floating point inputs and formally verifying the hardware design is recurrent over sets of β input exponents comprises:
formally verifying that the hardware design maintains a predetermined relationship between positive and negative floating point inputs; and
formally verifying that for any two non-exception positive floating point inputs, or for any two non-exception negative floating points inputs, that have the same input mantissa and have input exponents X and Y that differ by an integer multiple of β the corresponding floating point outputs produced by the hardware design have the same output mantissa and have output exponents X′ and Y′ that satisfy the equation X′−t·X=Y′−t·Y.

4. The method of claim 1 , wherein the hardware design has a first recurrent input range comprising positive floating point inputs and a second recurrent input range comprising negative floating point inputs and formally verifying the hardware design is recurrent over sets of β input exponents comprises:
formally verifying that for any two non-exception positive floating point inputs that have the same input mantissa and have input exponents X and Y that differ by an integer multiple of β the corresponding floating point outputs have the same output mantissa and have output exponents X′ and Y′ that are satisfy the equation X′−t·X=Y′−t·Y; and
formally verifying that for any two non-exception negative floating points inputs that have the same input mantissa and have input exponents A and C that differ by an integer multiple of β the corresponding floating point outputs have the same output mantissa and have output exponents A′ and C′ that satisfy the equation A′−t·A=C′−t·C.

5. The method of claim 1 , further comprising formally verifying that the hardware design generates expected outputs in response to exception inputs.

6. The method of claim 1 , further comprising formally verifying that the hardware design produces exception outputs in response to certain non-exception inputs.

7. The method of claim 1 , wherein formally verifying that the hardware design is recurrent over sets of β input exponents comprises verifying, using a formal verification tool, the one or more formal assertions.

8. The method of claim 1 , wherein the property of the hardware design is a unit of last precision error requirement.

9. The method of claim 1 , wherein the property of the hardware design is a relative error requirement.

10. The method of claim 1 , wherein the property of the hardware design is a particular rounding mode.

11. The method of claim 1 , wherein the property of the hardware design is monotonicity.

12. The method of claim 1 , wherein the property of the hardware design is that the hardware design is equivalent to another hardware design to implement the floating point power function.

13. The method of claim 1 , wherein when the hardware design is processed at an integrated circuit manufacturing system, the hardware design configures the integrated circuit manufacturing system to manufacture an integrated circuit to implement the floating point power function.

14. A method of generating a hardware implementation of a floating point power function comprising:
receiving a hardware design to implement the floating point power function;
verifying a property of the hardware design according to the method as set forth in claim 1 ; and
generating a hardware implementation of the floating point power function based on the hardware design.

15. A method of generating a hardware implementation of a floating point power function comprising:
receiving a hardware design to implement the floating point power function;
verifying a property of the hardware design according to the method as set forth in claim 1 ;
in response to the property of the hardware design not being verified, amending the hardware design; and
generating a hardware implementation of the floating point power function based on the amended hardware design.

16. A system to exhaustively verify a property of a hardware design to implement a floating point power function defined by an exponent, the hardware design being configured to, in response to receiving a floating point input that has an input mantissa and an input exponent, produce a corresponding floating point output that has an output mantissa and an output exponent, the system comprising:
a formal verification tool configured to formally verify that the hardware design is recurrent over sets of β input exponents, the hardware design being recurrent over sets of β input exponents if for any two non-exception floating point inputs in a recurrent input range that have the same input mantissa and have input exponents X and Y that differ by an integer multiple of β the corresponding floating point outputs produced by the hardware design have the same output mantissa and have output exponents X′ and Y′ that satisfy the equation X′−t·X=Y′−t·Y, wherein t is the exponent of the floating point power function and β is an integer that is a multiple of 1/t; and
a simulation engine configured to, for each recurrent input range of the hardware design, exhaustively simulate the hardware design over a simulation range to verify the property over the simulation range, wherein the simulation range comprises floating point inputs based on a set of β input exponents in the recurrent input range.

17. The system of claim 16 , wherein the set of β input exponents comprises an input exponent from each of a plurality of exponent classes, each exponent class comprising input exponents with a same value modulo β.

18. The system of claim 16 , wherein the hardware design has a single recurrent input range that comprises positive and negative floating point inputs and the formal verification tool is configured to formally verify the hardware des

Assignees

• Imagination Tech Ltd

Inventors

• Elliott Sam

Classifications

• G06F2119/18

  Manufacturability analysis or optimisation for manufacturability · CPC title

• G06F30/20

  Design optimisation, verification or simulation (optimisation, verification or simulation of circuit designs G06F30/30) · CPC title

• G06F30/3323 Primary

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

• G06F7/556

  Logarithmic or exponential functions · CPC title

• G06F7/483 Primary

  Computations with numbers represented by a non-linear combination of denominational numbers, e.g. rational numbers, logarithmic number system or floating-point numbers {(G06F7/4806, G06F7/4824, G06F7/49, G06F7/491, G06F7/544 take precedence)} · CPC title