References:

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

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

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

[4]
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

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

[6]
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

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

[8]
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

[9].
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

[10]
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]

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

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

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

[14]
Simon Haykin, Communication Systems, Wiley Publishing, 2009

[15]
HOL Sourceforge Project. The HOL System Description. September 2005

[16]
HOL Sourceforge Project. The HOL System Reference. September 2005

[17]
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]

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

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

[20]
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.

[21]
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]

[22]
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

[23]
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

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

[25]
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

[26]
http://www.maplesoft.com

[27]
http://www.wolfram.com

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

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

[30]
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

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

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

[33]
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

[34]
http://www.xilinx.com/ipcenter

[35]
http://www.xilinx.com/ipcenter/coregen