Formal Methodology Validates Cache-Coherence Protocol

摘要

Sun's experience shows that a commercial formal property-checking tool can be very adept at architecture-level protocol checking. By using SystemVerilog and JasperGold, Sun's engineers exposed, clarified, and verified micro-architectural issues that were added to the architectural specification. The main benefit was increased confidence in the architecture and micro-architecture.