We describe the refinement of a directory based cache coherence protocol specification, to a pipelined hardware implementation. The hardware that is analyzed is the most complex part of a 1M-gate ASIC. The design consists of 30000 lines of synthesizable register transfer-level verilog code. The design contains a pipeline that is 5 levels deep and approximately 150 bits wide. It has a 16 entry, 150 bit wide, context addressable memory (CAM), and has a 256x72 bit RAM. Refinement maps relate the high-level protocol model to the hardware implementation. We used the Cadence Berkeley Labs SMV model checker to create the maps and to prove their correctness. There are approximately 2000 proof obligations. The formal model has been used for three tasks. First, to formally diagnose, and then fix broken features in a legacy version of the design. Second, to integrate the legacy sub-system design with a new system design. Finally, it has been used to formally design additional subsystem features required for the new system design. The same hardware designer enhanced the design, created the refinement maps, and formally proved the correctness of the refinements.