Modular Design As Algebraic Composition

The aim of this research is to study how high-level mathematical abstractions could be used for reasoning about hardware design. These abstractions will be used as the foundation for a CAD tool for VLSI. Of course, different algebraic abstractions are appropriate on different levels of the design hierarchy. Uncovering formalising and integrating these will be difficult but is necessary for the development of future CAD tools. We have developed a general algebra, applicable at all levels of the hierarchy, for composing small modules into large designs. Having a common composition algebra throughout allows transformations between levels (both refining transformations downwards and verification and abstraction transformations upwards) to be algebraic morphisms. In this paper, we present a sketch of the composition algebra, and closely follow a design at the behavioural level. It is hoped to give an indication both of the use of composition and of the kind of verification that can be done at the highest levels.