A methodology for early validation of cache coherence protocols based on relational databases

A novel, table-driven approach based on relational database technology is proposed for the design and early validation of cache coherence protocols. A protocol is specified as multiple communicating, multi-input, multi-output, finite-state machines each represented by a relational database table. The tables are automatically generated by solving relational calculus constraints specifying the protocol transactions. Early protocol validation prior to an implementation is performed by testing these tables for several protocol properties expressed using relational queries and database integrity constraints. The debugged tables are automatically mapped to a high-level hardware implementation while preserving their correctness. The proposed approach has been deployed at Fujitsu Systems Technology Division for the design of their next-generation multiprocessor and has been highly successful in reducing the overall protocol development time and has discovered several errors early in the design cycle. Copyright © 2006 John Wiley & Sons, Ltd.