Error Analysis and Verification of an IEEE 802.11 OFDM Modem using Theorem Proving

IEEE 802.11 is a widely used technology which powers many of the digital wireless communication revolutions currently taking place. It uses OFDM (Orthogonal Frequency Division Multiplexing) in its physical layer which is an efficient way to deal with multipath, good for relatively slow time-varying channels, and robust against narrowband interference. In this paper, we formally specify and verify an implementation of the IEEE 802.11 standard physical layer based OFDM modem using the HOL (Higher Order Logic) theorem prover. The versatile expressive power of HOL helped us model the original design at all abstraction levels starting from a floating-point model to the fixed-point design and then synthesized and implemented in FPGA technology. We have been able to find a bug in one of the blocks of the design that is responsible for modulation which implementation diverts from the constellation provided in the IEEE standard specification. The paper also derives new expressions for the rounding error accumulated during ideal real to floating-point and fixed-point transitions at the algorithmic level and performs a formal error analysis for the OFDM modem in HOL.