- In 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..
 Download
postscript file (PDF
File) |
| Send comments
and suggestions to: habibi@ece.concordia.ca |