Formal Error Analysis and Verification of the Frequency Domain Equalizer

Technical Report

Abstract
In this work we provide formal verification of a frequency domain equalizer using theorem proving techniques in Higher Order Logic framework. We perform formal error analysis to verify an implementation of the equalizer based on the Fast LMS algorithm. The formal error analysis is performed at the floating-point, fixed-point, and real numbers domains. The expressiveness of HOL allows us to model the equalizer in all the three number domains. The errors generated by approximating the floating-point and the fixed-point designs to the real domain were used to complete the error analysis of the frequency domain equalizer by deducting the error between the floating-point and the fixed-point formalizations of the design. This application shows the efficiency of formal methods in verifying complex system such as the frequency domain equalizer.

Files

• Technical Report: PDF File
• Appendix (HOL Theorems): PDF File