Formal error analysis and verification of a frequency domain equalizer

In this paper we provide an approach for the formal verification of a frequency domain equalizer using higher-order logic based theorem proving. We perform a multi-level formal error analysis to verify an implementation of the equalizer based on the Fast LMS (Least Mean Square) algorithm. The formal error analysis is performed at the floating-point, fixed-point, and real numbers domains. The expressiveness of higher-order logic allows us to model the equalizer in all the three number domains and valuate the errors generated by approximating the floating-and fixed-point designs to the real domain of the frequency domain equalizer. This application shows the efficiency of formal methods in analyzing and verifying complex systems such as the frequency domain equalizer.