Formal Verificaction of the ADSP-2100 Processor Using the HOL Theorem Prover
Ali Habibi, Sofiène Tahar, Adel Ghazel · 2002
In this technical report, we present the application of formal verification to digital signal processors of the family ADSP-2100 using the HOL (Higher Order Logic) theorem prover. To solve the problem of complexity related to the big number of parameters of the processor, we used a structured method based on our knowledge about this processors family. In this method, we worked on the units of the processor as separate sub-systems in order to simplify their specifications by omitting the internal signals. We showdetails of the specification and verification strategies used and displayexperimental results as well the lessons learned.