Login | Register

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


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

Abdullah, Abu Nasser Mohammed, Akbarpour, Behzad and Tahar, Sofiène (2009) Error Analysis and Verification of an IEEE 802.11 OFDM Modem using Theorem Proving. Electronic Notes in Theoretical Computer Science, 242 (2). pp. 3-30. ISSN 15710661

[thumbnail of ENTCS-2009.pdf]
Text (application/pdf)
ENTCS-2009.pdf - Accepted Version

Official URL: http://dx.doi.org/10.1016/j.entcs.2009.06.020


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.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Article
Authors:Abdullah, Abu Nasser Mohammed and Akbarpour, Behzad and Tahar, Sofiène
Journal or Publication:Electronic Notes in Theoretical Computer Science
Digital Object Identifier (DOI):10.1016/j.entcs.2009.06.020
Keywords:error analysis; formal verification; ofdm; theorem proving; wireless communication
ID Code:977368
Deposited By: Danielle Dennie
Deposited On:14 Jun 2013 14:21
Last Modified:18 Jan 2018 17:44


A.N.M. Abdullah. Formal Analysis and Verification of an OFDM Modem. Master's thesis, Department of ECE, Concordia University, Montreal, QC, Canada, 2006

Behzad Akbarpour, Modeling and verification of dsp designs in hol, Concordia University, Montreal, P.Q., Canada, 2005

Peter J. Ashenden, The Designer's Guide to VHDL, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2001

Richard J. Boulton , Andrew Gordon , Michael J. C. Gordon , John Harrison , John Herbert , John Van Tassel, Experience with Embedding Hardware Description Languages in HOL, Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, p.129-156, June 22-24, 1992

Cadence Design Systems Inc. Signal Processing Worksystems (SPW) User's Guide, July 1999

A.L. Cinquino. A Real-Time Software Implementation of an OFDM Modem Suitable for Software Defined Radios. Master's thesis, Department of ECE, Concordia University, Montreal, QC, Canada, 2004

Forsythe, G. and Moler, C.B., Computer Solution of Linear Algebraic Systems. 1967. Prentice-Hall.

F. Frescura, S. Andreoli, S. Cacopardi, and E. Sereni. An OFDM Radio Transmitter based on TMS320C6000 DSP for Telemetry Applications. In Proceeding of International Conference Signal Processing Applications and Technology, Dallas, Texas, USA, October 2000

M. J. C. Gordon , T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, New York, NY, 1993

John Harrison, Constructing the real numbers in HOL, Formal Methods in System Design, v.5 n.1-2, p.35-59, July 1994 [doi>10.1007/BF01384233]

J. Harrison. Floating Point Verification in HOL Light: the Exponential Function. Technical Report 428, University of Cambridge Computer Laboratory, Cambridge, UK, 1997

J. Harrison. Complex Quantifier Elimination in HOL. In Supplemental Proceedings of Theorem Proving in Higher Order Logics, pages 159--174. Edinburgh, UK, September 2001

Osman Hasan, Formal probabilistic analysis using theorem proving, Concordia University, Montreal, P.Q., Canada, 2008

Simon Haykin, Communication Systems, Wiley Publishing, 2009

HOL Sourceforge Project. The HOL System Description. September 2005

HOL Sourceforge Project. The HOL System Reference. September 2005

M. Huhn , K. Schneider , Th. Kropf , G. Logothetis, Verifying imprecisely working arithmetic circuits, Proceedings of the conference on Design, automation and test in Europe, p.13-es, January 1999, Munich, Germany [doi>10.1145/307418.307451]

J. Hurd. Formal Verification of Probabilistic Algorithms. PhD thesis, University of Cambridge, Cambridge, UK, 2002

IEEE 802.11 Working Group. IEEE Std 802.11a-1999. The Institute of Electrical and Electronics Engineers, Inc, 1999

Jackson, L.B., Roundoff-Noise Analysis for Fixed-Point Digital Filters Realized in Cascade or Parallel Form. IEEE Transactions on Audio and Electroacoustics. vAU-18. 107-122.

Toyohisa Kaneko , Bede Liu, Accumulation of Round-Off Error in Fast Fourier Transforms, Journal of the ACM (JACM), v.17 n.4, p.637-654, Oct. 1970 [doi>10.1145/321607.321613]

Marta Z. Kwiatkowska , Gethin Norman , David Parker, PRISM: Probabilistic Symbolic Model Checker, Proceedings of the 12th International Conference on Computer Performance Evaluation, Modelling Techniques and Tools, p.200-204, April 14-17, 2002

Marta Z. Kwiatkowska , Gethin Norman , Jeremy Sproston, Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol, Proceedings of the Second Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification, p.169-187, July 25-26, 2002

Liu, B. and Kaneko, T., Error analysis of digital filters realized with floating-point arithmetic. Proceedings of the IEEE. v57. 1735-1747.

F. Manavi. Implementation of OFDM Modem for the Physical Layer of IEEE802.11a Standard Based on XILINX VIRTEX-II FPGA. Master's thesis, Dept. of ECE, Concordia University, Montreal, QC, Canada, 2004



Richard van Nee , Ramjee Prasad, OFDM for Wireless Multimedia Communications, Artech House, Inc., Norwood, MA, 2000

Roy, A. and Gopinath, K., Improved Probabilistic Models for 802.11 Protocol Verification. In: LNCS, 3576. Springer-Verlag. pp. 239-252.

M. Tariq, Y. Baltaci, T. Horseman, M. Butler, and A. Nix. Development of an OFDM based High Speed Wireless LAN Platform using the TI C6x DSP. In Proccedings of IEEE International Conference on Communications, pages 522--526, New York, NY, USA, May 2002

Thong, T. and Liu, B., Fixed-point fast fourier transform error analysis. ASSP. v24 i6. 563-573.

James H. Wilkinson, Rounding Errors in Algebraic Processes, Dover Publications, Incorporated, 1994

Wai Wong, Modelling Bit Vectors in HOL: the word library, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, p.371-384, August 11-13, 1993


All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top