An Algebraic Approach to Hardware Description and Verification

From bibtex.

Abstract

We apply algebraic techniques to various aspects of hardware description and verification, with particular emphasis on VLSI (Very Large Scale Integration) circuit design. A simple and uniform notation for the description of networks of hardware components is introduced. It is shown how to impose planarity constraints, and how to treat regular and repetitive structures in convenient ways. The notation is applied to several examples of hardware networks. All these examples constitute different levels of description in the process of translating behavioural specifications into VLSI circuits. A formal semantics is given for the topmost level. Algorithms are given for the translation of purely topological planar stick expressions into metric structures from which layouts can be generated. The implementation of an experimental VLSI design system is described which uses algebraic concepts to hide detailed geometrical information. Geometric layouts are introduced as an abstract data type in a general purpose functional programming language and considerable advantages over traditional design systems are demonstrated with respect to the user interface. On the semantic side, two different formal frameworks are defined for the description of systems developing in continuous time. The emphasis is again algebraic, and techniques of both denotational and operational semantics are used. In the operational framework nondeterministic systems can be treated in a natural way, and it is possible to precisely formulate the behaviour of synchronous and asynchronous systems and to study their interactions.