Abdullah, Abu Nasser Mohammed (2006) Formal analysis and verification of an OFDM modem design. Masters thesis, Concordia University.
MR14272.pdf - Accepted Version
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.
|Divisions:||Concordia University > Faculty of Engineering and Computer Science > Electrical and Computer Engineering|
|Item Type:||Thesis (Masters)|
|Authors:||Abdullah, Abu Nasser Mohammed|
|Pagination:||xiii, 136 leaves : ill. ; 29 cm.|
|Degree Name:||M.A. Sc.|
|Program:||Electrical and Computer Engineering|
|Thesis Supervisor(s):||Tahar, Sofiène|
|Deposited By:||Concordia University Libraries|
|Deposited On:||18 Aug 2011 18:33|
|Last Modified:||05 Nov 2016 00:52|
Repository Staff Only: item control page