A Top Down Approach to the Formal Specification of SCI Cache Coherence