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.

. Many modern systems are designed as a set of interconnected reactive subsystems. The subsystem verification task is to verify an implementation of the subsystem against the simple deterministic high-level specification of the entire system. Our verification methodology, based on Symbolic Trajectory Evaluation, is able to bridge the wide gap between the abstract specification and the implementation specific details of the subsystem. This paper presents a detailed description of an industrial application of this methodology to the fixed point execution unit of the PowerPC processor. We were able to verify a representative instruction under all possible stall, bypass, pipeline conditions and under all possible timings for interface to other functional units in the processor. 1. Introduction Some modern systems with a simple deterministic high-level specification have implementations that exhibit highly nondeterministic behaviors. A large class of systems that exhibit such...