Integrating design and verification of digital integrated circuits

Formal methods have an important role to play in the management of design information and in proving design correctness. The need is for formality to be introduced into the design process and not just to be used in post design validation. The use of relations to describe behaviour and functional style combining forms to describe circuit structure is a useful framework in which to design formally. A simple example of specifying circuit behaviour is given. The machine behaviour is specified as a group of relations between states. These are then related to compositions of combining forms which succinctly describe the structure of the circuits being designed. The work described in the paper suggests that this approach can be usefully extended to describing and designing general circuits such as microcontrollers and microprocessors