System, method, and computer program product for hierarchical formal hardware verification of floating-point division and/or square root algorithmic designs using automatic sequential equivalence checking

A method, comprising:

• identifying, for at least one of a floating-point division algorithm and a square root algorithm, an architectural specification for hardware, a hardware implementation on the hardware, and at least one intermediate model having a level of specificity between the architectural specification and the hardware implementation;
• automatically determining, via an automatic sequential equivalence determination executed by a processor, an equivalence, hierarchically, between the architectural specification, the at least one intermediate model, and the hardware implementation;
• and
• formally verifying, for the hardware, the at least one of the floating-point division algorithm and the square root algorithm, based on the automatic sequential equivalence determination,
• wherein automatically determining the equivalence, hierarchically, between the architectural specification, the at least one intermediate model, and the hardware implementation includes:
• a) determining the equivalence between the architectural specification and a first one of the at least one intermediate model having a first level of specificity from the architectural specification;
• b) in response to determining that the architectural specification and the first one of the at least one intermediate model are equivalent, for each subsequent one of the at least one intermediate model having an incrementally greater level of specificity than a previous one of the at least one intermediate model:
• i) determining the equivalence between the subsequent intermediate model and the previous intermediate model;
• c) in response to determining that each subsequent intermediate model is equivalent to the previous intermediate model, determining the equivalence between the hardware implementation and a last one of the intermediate models having a greatest level of specificity from the architectural specification.

A computer program product embodied on a non-transitory computer readable medium, comprising:

• computer code for identifying a set of algorithmic designs including an architectural specification for a hardware design having a first level of specificity, a hardware implementation having a second level of specificity, and at least one intermediate model having a level of specificity between the first level of specificity and the second level of specificity;
• computer code for automatically determining, via an automatic sequential equivalence determination executed by a processor, whether the architectural specification, the at least one intermediate model, and the hardware implementation are equivalent;
• and
• computer code for formally verifying the hardware design based on the automatic sequential equivalence determination,
• wherein the hardware design implements at least one of a floating-point division algorithm and a square root algorithm.

An apparatus, comprising:

• a processor for:
• identifying a set of algorithmic designs including an architectural specification for a hardware design having a first level of specificity, a hardware implementation having a second level of specificity, and at least one intermediate model having a level of specificity between the first level of specificity and the second level of specificity;
• automatically determining, via an automatic sequential equivalence determination executed by the processor, whether the architectural specification, the at least one intermediate model, and the hardware implementation are equivalent;
• and
• formally verifying the hardware design based on the automatic sequential equivalence determination,
• wherein the hardware design implements at least one of a floating-point division algorithm and a square root algorithm.