Akbarpour, Behzad (2005) Modeling and verification of DSP designs in HOL. PhD thesis, Concordia University.
|PDF - Accepted Version|
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)|
|Pagination:||xi, 136 leaves : ill. ; 29 cm.|
|Degree Name:||Ph. D.|
|Program:||Electrical and Computer Engineering|
|Thesis Supervisor(s):||Tahar, Sofiène|
|Deposited By:||Concordia University Libraries|
|Deposited On:||18 Aug 2011 14:25|
|Last Modified:||18 Aug 2011 15:30|
Repository Staff Only: item control page