A methodology for formal design of hardware control with application to cache coherence protocols
Cindy Eisner, Irit Shitsevalov, Russ Hoover, Wayne G. Nation, Kyle L. Nelson, Ken Valk · 2000
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 st yle, is executable, formally verified, and automatically translated into HDL, thus giving hardware which is by construction equivalen t to its specification. We discuss the application of this methodology as it is used in product development of cache coherence protocols.