The Jasper User Group Meeting was held on November 8 & 9 and was full of presentations on the diverse ways that users are applying formal techniques — some in areas where never before thought possible. Paul Martin from ARM was one of those users who presented on this topic. ARM discussed how modern multi-core processors now require much more sophisticated cache control than before, ensuring that all devices in the system have the same view of shared data, known as cache coherency. ARM in particular has created some quite sophisticated protocols, AXI Coherency Extensions (ACE), under the AMBA 4 umbrella, that they announced at DAC.The need to move cache management to hardwareIn the old days, cache coherency management was largely done in software, invalidating large parts of the cache to ensure no stale data could get accessed, and forcing the cache to gradually be reloaded from main memory. There are several reasons why this is no longer appropriate. Caches have got very large and the penalty for off-chip access back to main memory is enormous. A large amount of data flowing through a slow interface is bad news for system performance, and off chip memory accesses have a big negative impact on power.Caches now require more intelligence. Instead of invalidating lots of data that might turn out to be 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. This even needs to be extended to devices that don't even have caches since a DMA device cannot simply go to the main memory due to delayed write-back.Verifying the AMBA4 protocol with Jasper's ActiveModel Obviously these protocols are pretty complicated, so how do you verify them? It's not just about verifying that a given RTL implementation of the protocol is good, that is the normal verification problem that formal and simulation techniques have been used on for years. It's about verifying that the protocol itself is correct. In particular, that the caches are coherent (any reader correctly gets the last write) and deadlock-free (all operations will eventually complete, or a weaker condition, at least one operation can always make progress).ARM discussed how they addressed this issue using Jasper's ActiveModel table-driven formal technology. This creates a circuit that is a surrogate for the protocol. Yes, it has registers and gates but these are not something implementable, they capture the fundamental atomic operations in the protocol. Then, using standard proof techniques, this circuit can be analyzed to make sure it has the good properties that it needed.It was a worthwhile exercise. It turned out that the original spec contained some errors. Of course they were weird corner cases, but that is what formal verification is so good at. Simulation hits the stuff you already thought of. There was one circumstance under which the whole cache infrastructure could deadlock, and another in which it was possible to get access to stale data. There is a white paper for download, a video for viewing and a blog that discusses this very topic.
Guest Partner Blogger:
Lawrence Loh, Vice President of Worldwide Applications Engineering at Jasper Design Automation, holds overall management responsibility for the company's applications engineering and methodology development. Loh has been with the company since 2002, and was formerly Jasper's Director of Application Engineering. He holds four U.S. patents on formal technologies. His prior experience includes verification and emulation engineering for MIPS, and verification manager for Infineon's successful LAN Business Unit. Loh holds a BSEE from California Polytechnic State University and an MSEE from San Diego State.