ARM Community: Upgrading Your Verification For Cache Coherency With Jasper! - ARM Community

Are you using a mobile device? Chances are you’re probably reading this blog post on one. You’re also probably reading this with the confidence that your device is doing what you intend it to do. As consumers, we place a lot of demands on not only our mobile devices but also the rest of our personal electronics. We want them to perform all sorts of tasks efficiently, accurately, and with minimal power consumption. As an engineer, you’re aware of the complex embedded SoC’s used in your device to make sure that it does what’s intended. Today’s embedded SoC’s are high performance, heterogeneous, and multi-processing systems.

In the future, most of these embedded SoC’s are likely to contain multiple caches that share a single memory resource. At a high level, cache coherency means that two caches cannot have same cache line in a dirty state and that if a cache contains a cache line in a unique state, that line must not be in another cache. In addition, at least one transaction must always be able make forward progress (no deadlock.) To prevent these cache coherency issues, ARM has included cache coherence extensions in their AMBA 4 protocol specification.

While this is a tremendous benefit, questions of how cache coherency is verified are raised. Jasper Design Automation has worked closely with ARM to rigorously validate the protocol using Jasper’s unique formal technology. The result is twofold: ARM is able to deliver the protocol specifications with high confidence and ARM licensees can use the verification IP and methodology that was used at ARM in the verification of their own SoC.

Cache coherency verification entails several challenges. Capturing the intent of the specification by transferring intent from the specification into a machine-readable format that can be processed can produce errors. When proving all possible scenarios, using only simulation is impractical because the state space is too large and it is impossible for dynamic verification systems to generate comprehensive stimuli. Using simulation can also result in long debug times. During debug, a presentation of conflicts or errors in functional terms is abstracted from the waveform. The errors then need to somehow be correlated to the specifications.

Leveraging the results of the work Jasper did with ARM you can upgrade your verification of SoC’s using cache coherency to avoid these shortcomings. Below is a high-level description of the collaboration between Jasper and ARM on the verification of cache coherency.

Verification of the protocol specifications was the first step. The natural language specifications were converted into declarative specifications in Jasper ActiveModel™. This enabled a rigorous analysis of each specification item and helped resolve possible inconsistencies. Verilog model and properties were then generated from the declarative specifications and additional validation of the specifications was performed with JasperGold®. The next step was to add the high-level coherency requirements and validate that the protocol, as specified, does indeed conform to the intent. Using JasperGold, the verification team was able to prove that the protocol, as specified, complies. The Verilog model generated by ActiveModel then becomes the reference model for ACE. This model is query-able, allowing users to visualize and understand the flow of ACE transactions.

Traditionally, creating system-level reference models by monitoring transactions at the interface level is difficult and thus not done. Therefore, you would have had to map the internal components of the RTL for refinement mapping, causing the high-level model to be design dependent. By using Jasper’s formal technology to create the model at the interface level allowed us to directly use the ACE protocol verification model as the ACE-System proof kit to verify the RTL. We were able to use the assumptions generated from the model as assertions to check that the RTL complies with the reference model. Because we were able to specify an interface model, any component that connects to the ACE system can be verified with ease. If the system-level assertions are followed, the coherency is maintained.

The collaboration with ARM not only validated the specification, but also resulted in certification of Jasper’s system-level verification IP (VIP) for ACE. This VIP addresses other issues beyond cache coherency such as absence of deadlocks. There is also a query-able ACE model that was developed to enable you to comprehend the ACE specification and help answer your system-level design questions.

The efforts that have been taken by Jasper and ARM will go a long way to reducing the risks you take in your design and verification efforts. To help you better understand the available technology, ARM and Jasper have partnered together to develop a set of whitepapers to address the issues of cache coherency and verification. Links to these whitepapers can be found below. We also invite you to hear firsthand what this technology and methodology are all about by attending our seminar in the Jasper booth #1931 at DAC.

• Jasper whitepaper on cache coherency verification
• ARM whitepaper on cache coherency
  

Also, find out more about the new ARM SoC Design Community!

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.

ARM welcomes its wealth of Partners in the ARM Connected Community (CC) to submit guest blogs to be published on our multiple community blogs. If interested in participating please submit email inquiries to Tell.Us@arm.com.

The ARM Connected Community (CC) is an extensive ecosystem covering all aspects of ARM processor-based design, from chip implementation through to system and device design. The CC provides a platform for collaborative innovation, with multiple types of forums for members to work with one another, and with customers, to solve industry challenges, all with the purpose of enabling designers to focus on differentiating features and an accelerated time-to-market for ARM powered solutions.