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.