DocumentCode :
3106736
Title :
Formal methods for silicon compilation
Author :
Kalker, Ton
Author_Institution :
Philips Res. Labs., Eindhoven, Netherlands
fYear :
1991
fDate :
25-28 Feb 1991
Firstpage :
395
Lastpage :
400
Abstract :
At the Philips Research Laboratories there is a large research effort on silicon compilation for DSP applications. The PIRAMID system is a prototype compiler which is capable of going from specification to layout within a few hours. The input language for PIRAMID has an applicative nature and is called SILAGE. In order to reduce the number of mistakes made during specification a good formal semantics of SILAGE is an absolute necessity. A study into the feasibility of denoting the formal semantics of SILAGE in the mathematical notation of higher order logic revealed several weak points of SILAGE. This paper shows that using mathematical methods one can define a better (with respect to specification/verification purposes) version of SILAGE (SILAGE+) without really adding to the complexity of the PIRAMID compiler
Keywords :
circuit layout CAD; digital signal processing chips; program compilers; program verification; specification languages; DSP applications; PIRAMID system; SILAGE; compiler; formal semantics; higher order logic; silicon compilation; Clocks; Digital signal processing; Laboratories; Logic; Mathematics; Microprocessors; Prototypes; Silicon compiler; Streaming media; Very large scale integration;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Design Automation. EDAC., Proceedings of the European Conference on
Conference_Location :
Amsterdam
Type :
conf
DOI :
10.1109/EDAC.1991.206433
Filename :
206433
Link To Document :
بازگشت