Origin system design methodology and experience: 1M-gate ASICs and beyond

The Origin 2000 system from Silicon Graphics Inc. pushed the complexity limits of ASIC design to levels previously only seen in full custom microprocessors. We describe the methodology used to implement and verify this ccNUMA (cache coherent non-uniform memory access) multiprocessor system. A formal specification, consisting of a detailed machine-readable description of the ccNUMA cache coherence protocol was the cornerstone used to manage the complexity of the design. This specification was formally verified and used to automate logic verification. We used a hierarchical approach at all levels to attack the design and verification. We made design decisions to ease verification without compromising system performance. The completion of this system, running at speed, with no bugs in the cache coherence protocol, validates this methodology.