Breadcrumb

 
 

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.

[img]
Preview
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 > Faculty 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
ID Code:8433
Deposited By:Concordia University Libraries
Deposited On:18 Aug 2011 14:25
Last Modified:18 Aug 2011 15:30
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

Document Downloads

More statistics for this item...

Concordia University - Footer