Formal synthesis of VLSI layouts from algorithmic specifications

Due to advances in VLSI technology, it is possible to implement complex digital systems on a single chip. However modelling such large and complex systems at structural level is tedious and error prone. This fact has motivated the development of several high-level synthesis systems. The process consists of translating the abstract behavioural representation generally at the algorithmic level into a structural realizable representation. In this paper we present a formal approach for high-level synthesis. This formal high-level synthesis system uses μ-recursive algorithms to model the behaviour to be synthesized. These algorithms can be mathematically verified for correctness before being subjected to the task of translation. As a case study, the modelling and synthesis of VLSI layouts for matrix-matrix multipliers is discussed.