Methodology for formal design of hardware control with application to cache coherence protocols

We propose a methodology for developing hardware control. In addition to the usual distinction between control and data path, a further distinction within the control code is made between algorithmic code and bookkeeping code. The high level specification describes the algorithmic code in an object-oriented style, is executable, formally verified, and automatically translated into HDL, thus giving hardware which is by construction equivalent to its specification. We discuss the application of this methodology as it is used in product development of cache coherence protocols.