Verification of hardware designs to implement floating point power functions
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.
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 design is recurrent over sets of β input exponents by:
formally verifying that the hardware design maintains a predetermined relationship between positive and negative floating point inputs;
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.
19. The system of claim 16 , further comprising an integrated circuit manufacturing system configured to process the hardware design so as to manufacture an integrated circuit to implement the floating point power function.
20. The system of claim 19 , wherein the integrated circuit manufacturing system comprises:
a non-transitory computer readable storage medium having stored thereon the hardware design;
a layout processing system configured to process the hardware design so as to generate a circuit layout description of an integrated circuit to implement the floating point power function; and
an integrated circuit generation system configured to manufacture the integrated circuit to implement the floating point power function according to the circuit layout description.