Design and verification of regular synchronous circuits

A VLSI design language, µFP, is presented and it is shown how it can be used in the development of regular array circuits. The higher order functions which are used to build circuit descriptions have geometric as well as semantic interpretations. They allow common circuit forms to be described simply and concisely. The language obeys various algebraic laws, and circuits are developed by transforming a correct (but possibly inefficient) initial design into a more acceptable implementation. A transformation consists of the application of one or more of the algebraic laws and the final circuit is guaranteed to have the same behaviour as the original one. This algebraic approach to circuit design and verification is demonstrated by using it to develop several alternative systolic and semi-systolic implementations of a simple FIR filter.