Formal modelling of the ADSP-2100 processor using HOL
Ahmad Rizky Nusantara Habibi, Sofiène Tahar, Adel Ghazel · 2003
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.