About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
DAC 2000
Conference paper
Methodology for formal design of hardware control with application to cache coherence protocols
Abstract
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.