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
fDate :
6/24/1905 12:00:00 AM
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;
Conference_Titel :
Electrical and Computer Engineering, 2002. IEEE CCECE 2002. Canadian Conference on
Print_ISBN :
0-7803-7514-9
DOI :
10.1109/CCECE.2002.1013012
