Published Articles >> Table of Contents >> Abstract

Euromicro Symposium on Digital System Design (DSD'02)   p. 12
Formal Verification of a DSP Chip Using an Iterative Approach
Ali Habibi, Concordia University
Sofiene Tahar, Concordia University
Adel Ghazel, École Superieure Des Communications de Tunis

Full Article Text:

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/DSD.2002.1115346
Send link to a friend

Abstract
In this paper we describe a methodology for the formal verification of a DSP chip using the HOL theorem prover. We used an iterative method to specify both the behavioral and structural descriptions of the processor. Our methodology consists of first simplifying the representations of the DSP units. We then prove for each unit that its hardware description implies its behavioral specification. Using the simplified (abstracted) description of the units we have been able to greatly reduce the cost of deducing the behavior of the processor instruction set from the hardware implementation of the processor units. The proposed methodology creates a new representation of the processor at each iteration such that its complexity can be handled by the theorem prover. This allowed us to make a proof of the full instruction set of this processor.
Back to Top Additional Information
Citation:  Ali Habibi, Sofiene Tahar, Adel Ghazel, "Formal Verification of a DSP Chip Using an Iterative Approach," dsd, p. 12,  Euromicro Symposium on Digital System Design (DSD'02),  2002