Ifip transactions a-computer science and technology vol:20 pages:375-394
Silage is an applicative language for describing multi-rate DSP algorithms. It has been used as the high level input language to the CATHEDRAL Silicon Compilers. Hardware implementations of specifications described in Silage are synthesized and inconsistencies in the synthesis trajectory must be avoided. To build the foundations of a verification environment, the formal semantics of Silage must be defined. Our main motivation to formally define the semantics of Silage is to build formal tools, in such a way that the interactivity between the user and the silicon compiler can be increased in a safe way. The designer could then interactively transform the specification, fully exploiting his expertise, but without the risks of introducing inconsistencies. Formally verified transformational design techniques could then be applied at the specification level of the Silicon Compilers. This paper describes the formal semantics definition of a substantial subset of Silage focusing on the multi-rate aspects of the language.