Formal methods for silicon compilation

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