IBM Logo
IBM Research Lab in Haifa
 
Location  
Agenda  
 
 
Hot Shots  
 
FV Research in HRL  

Download the presentation

Cindy Eisner

IBM HRL

Abstract

A 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.