DocumentCode
3569560
Title
Formal modelling of the ADSP-2100 processor using HOL
Author
Habibi, Ali ; Tahar, Sofi?¨ne ; Ghazel, Adel
Author_Institution
Dept. of Electr. & Comput. Eng., Concordia Univ., Montreal, Que., Canada
Volume
2
fYear
2002
fDate
6/24/1905 12:00:00 AM
Firstpage
614
Abstract
In this paper we describe formal modelling of the digital signal processors of the family ADSP-2100 using the HOL (Higher Order Logic) theorem prover. While specifying the behavior and implementation of the processor we solved the problem of complexity related to the large number of parameters by using a structured method based on our knowledge about the processor architecture. We show details of the specification strategy used and display few illustrative examples.
Keywords
digital signal processing chips; formal specification; formal verification; theorem proving; ADSP-2100; Higher Order Logic; complexity; digital signal processors; formal methods; formal modelling; hardware verification; theorem prover; Computer architecture; Digital signal processing; Displays; Hardware; Humans; Logic design; Logic programming; Microprocessors; Signal processing; Software systems;
fLanguage
English
Publisher
ieee
Conference_Titel
Electrical and Computer Engineering, 2002. IEEE CCECE 2002. Canadian Conference on
ISSN
0840-7789
Print_ISBN
0-7803-7514-9
Type
conf
DOI
10.1109/CCECE.2002.1013012
Filename
1013012
Link To Document