Treffer: Enabling hardware verification through design changes

The IEEE-754 floating-point standard, used in nearly all floating-point applications, is considered as one of the most important standards. Deep datapath and algorithm complexity have made the verification of such floating-point units a very hard task. Theorem proving, offers a good solution to handle such verification tasks. In this paper, we stress on the design changes performed for the sake of formalizing and verifying the IEEE-754 table-driven exponential function in all abstraction levels of the design flow. While verifying the VHDL code implementation against a high-level abstract specification, we were faced by two main problems: (1) the large abstraction gap between the two models; and (2) the flatness of the VHDL code, making it intractable to model and formally verify. We have therefore proposed a hierarchical methodology to solve such modeling problem, and experimented it on our verification task using the HOL theorem proving environment.