At DAC Jasper presented a seminar with ARM on cache coherency and verification of cache coherency. The seminar is now available online for those of you that missed DAC or missed the seminar itself.
Cache architectures, especially for multi-core architectures, are getting more and more complex. Techniques originally pioneered on supercomputers are now finding their way into complex SoCs. The difference in performance between making an off-chip memory reference versus finding data in one of the caches already on the chip is so big that it is worth paying a price in additional complexity to add hardware that keeps caches coherent when data is written to one of them. But this complexity needs to have a good specification of exactly what the guarantees of coherency area, and a mechanism for verifying that the guarantees hold.
To view the seminar register here.
To request the white paper on the subject register here.