Login | Register

Modeling and verification of DSP designs in HOL

Title:

Modeling and verification of DSP designs in HOL

Akbarpour, Behzad (2005) Modeling and verification of DSP designs in HOL. PhD thesis, Concordia University.

[thumbnail of NR04055.pdf]
Preview
Text (application/pdf)
NR04055.pdf - Accepted Version
4MB

Abstract

In this thesis 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 (Higher Order Logic) 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 (Register Transfer Level), 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 (Fast Fourier Transform) algorithms.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (PhD)
Authors:Akbarpour, Behzad
Pagination:xi, 136 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:Ph. D.
Program:Electrical and Computer Engineering
Date:2005
Thesis Supervisor(s):Tahar, Sofiène
Identification Number:QA 76.9 A96A33 2005
ID Code:8433
Deposited By: Concordia University Library
Deposited On:18 Aug 2011 18:25
Last Modified:13 Jul 2020 20:04
Related URLs:
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