Early error detection in industrial strength cache coherence protocols using SQL

A table-driven approach for designing industrial strength cache coherence protocols based on relational database technology is described. Protocols are specified using several interacting multi-input, multi-output controller state machines represented as database tables. Protocol scenarios specified using SQL constraints are solved to automatically generate database tables, and to statically check protocol properties including absence of deadlocks and other protocol invariants. The debugged tables are mapped to hardware using SQL operations while preserving protocol properties. The approach is deployed at Fujitsu System Technology Division in the design of their next generation multiprocessor and has discovered several errors early in the design cycle.