In this project  we propose a framework for the incorporation of formal methods in the design flow of DSP (Digital Signal Processing) systems in a rigorous way. In the proposed approach we model and verify DSP descriptions at different abstraction levels using higher-order logic based on the HOL theorem prover. This framework enables the formal verification of DSP designs which in the past could only be done partially using conventional simulation techniques. To this end, we provide a shallow embedding of DSP descriptions in HOL at the floating-point, fixed-point, behavioral, RTL, and netlist gate levels. We make use of existing formalization of floating-point theory in HOL and introduce a parallel one for fixed-point arithmetic. The high ability of abstraction in HOL allows a seamless hierarchical verification encompassing the whole DSP design path, starting from top level floating- and fixed-point algorithmic descriptions down to RTL, and gate level implementations. We illustrate the new verification framework using different case studies such as digital filters and FFT algorithms.

Behzad Akbarpour

Dr. Sofiene Tahar

Behzad Akbarpour, "Modeling and Verification of DSP Designs in HOL," Ph.D. Thesis, Concordia University, Department of Electrical and Computer Engineering, April 2005.

B. Akbarpour, S. Tahar, and A. Dekdouk, “ Formalization of Fixed-Point Arithmetic in HOL”, Formal Methods in Systems Design, Vol. 27, pp. 173-200, Springer-Verlag, 2005.

B. Akbarpour and S. Tahar, “ An Approach for the Formal Verification of DSP Designs using Theorem Proving”, IEEE Transactions on CAD of Integrated Circuits and Systems, In-Print. [29 pages]

3. B. Akbarpour and S. Tahar, “ Error Analysis of Digital Filters using Theorem Proving ” , Submitted to Journal of Applied Logic, Elsevier. [35 pages]

B. Akbarpour and S. Tahar, "Incorporating Formal Methods in the Design Flow of DSP Systems," In Proceedings NETCA Workshop on Verification and Theorem Proving for Continuous Systems, Oxford, UK, August 2005.

 B. Akbarpour and S. Tahar, ``A Methodology for the Formal Verification of FFT Algorithms in HOL,'' In Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science, LNCS 3312, pp. 37-51, Springer-Verlag, 2004.

B. Akbarpour and S. Tahar, ``Error Analysis of Digital Filters using Theorem Proving,'' In Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, LNCS 3223, pp. 1-16, Springer-Verlag, 2004.

 B. Akbarpour and S. Tahar, ``Modeling SystemC Fixed-Point Arithmetic in HOL,'' In Formal Methods and Software Engineering, Lecture Notes in Computer Science, LNCS 2885, pp. 206-225, Springer-Verlag, 2003.

B. Akbarpour and S. Tahar, ``The Application of Formal Verification to SPW Designs,'' In Proceedings Euromicro Symposium on Digital System Design, IEEE Computer Society Press, pp. 325 -332, Belek, Turkey, September 2003. 

6. B. Akbarpour, S. Tahar, and A. Dekdouk, ``Formalization of Cadence SPW Fixed-Point Arithmetic in HOL,'' In Integrated Formal Methods, Lecture Notes in Computer Science, LNCS 2335, pp. 185-204, Springer-Verlag, 2002.

B. Akbarpour and S. Tahar: Formalization of Fixed-Point Arithmetic in HOL, Technical Report, Concordia University, Department of Electrical and Computer Engineering, September 2002.

B. Akbarpour , and S. Tahar: Error Analysis of Digital Filters using HOL Theorem Proving; Technical Report, Concordia University, Department of Electrical and Computer Engineering, February 2004. [36 pages]

B. Akbarpour , and S. Tahar: Verification of the Fast Fourier Transform using HOL Theorem Proving; Technical Report, Concordia University, Department of Electrical and Computer Engineering, March 2004. [40 pages]