Formal analysis and verification of an OFDM modem design

In this thesis we formally specify and verify an implementation of the Orthogonal Frequency Division Multiplexing (OFDM) Physical Layer using theorem proving techniques based on the HOL (Higher Order Logic) system. The thesis is meant to follow a framework, developed at Concordia University, incorporating formal methods in the design flow of digital signal processing systems in a rigorous way. The design under verification is a prototype of IEEE 802.11 Physical Layer implemented using standard Very Large Scale Integration (VLSI) design flow, starting from a floating-point model to the fixed-point and then synthesized and implemented in Field Programmable Gate Array (FPGA) technology. The models were verified in HOL against the IEEE 802.11 specification ratified by the IEEE standardization body and implemented by almost all major wireless industry in the world. The versatile expressive power of HOL helped model the original design at all abstraction levels without affecting its integrity. (Abstract shortened by UMI.)...