January 11, 2012 -- Consumer demand for increasing functionality in devices has resulted in multi-core processors requiring more sophisticated cache control. The presence of a large number of data-processing agents sharing a memory resource on a system-on-chip (SOC) requires that the agents maintain some type of locally cached data to reduce the data-transportation cost. This, in turn, leads to the requirement for cache coherency to allow agents to cache data during processing and then make it available to the next processing agent. Today's caches need to be intelligent in the sense that instead of invalidating lots of data that might turn out stale, the cache controllers need to invalidate on a line-by-line basis in order to ensure that anybody reading an address gets the latest value written.

How can one accomplish this? We explore this question in this article using a unique, existing formal technology that can provide a method for modeling and verifying cache-coherent protocols, with an ARM AMBA AXI Coherency Extensions (ACE) protocol. We demonstrate how to develop and verify system- and interface-level VIP for the ARM ACE protocol.

By Rajeev Ranjan. (Ranjan develops Jasper Design Automation's overall technology vision and drives the business value of formal verification.)