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 system, method, and computer program product are provided for hierarchical formal hardware verification of floating-point division and/or square root algorithmic designs using automatic sequential equivalence checking. In use, 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 are identified. Additionally, an equivalence is automatically determined, hierarchically, between the architectural specification, and the at least one intermediate model, and between the at least one intermediate model and the hardware implementation. Furthermore, for the hardware, the at least one of the floating-point division algorithm and the square root algorithm are formally verified, based on the automatic sequential equivalence determination.