Formal Techniques for Protocol Verification: A Case Study On Verifying the ARM ACE Protocol

1 of Enlarge image

Fig 1. One means of creating a model for the ARM ACE protocol is with Jasper Design Automation’s ActiveModel table-based entry format. The format is similar to those used by many cache-coherent protocol specifications.

Fig 2. To understand a failure trace from a protocol model, it is often beneficial to have a high-level view of what is occurring. ActiveModel creates a link from a failing property to the appropriate rows in the table.

Fig 3. A technology for eliminating unimportant transactions from a waveform showing a violation, appropriately called QuietTrace, is available when using ActiveModel. This example shows two waveforms, each showing all the row covers that were active in the violation trace. The first appears without quieting of the waveform; it shows 50 firings of the row covers. The second is the equivalent trace obtained by QuietTrace technology. It shows only 13 firings of the covers. The 13 row covers are all likely contributing to the violation, drastically improving debug efficiency.

Fig 4. Visualizing cases to build comprehension is a perfect application for the ACE ActiveModel. This example shows visualization of a row indicating that a ReadShared snoop is hitting a UC line.

Fig 5. Following on from Figure 4, the tool quickly generates the nine-cycle waveform showing the desired flow.

Fig 6. Here are two steps to the process of determining whether WasUnique and DataTransfer can be active on a snoop response. The upper waveform shows the “Add Constraint” dialog in which we modify the default expression. The lower waveform shows the results after replotting the waveform. The replotted waveform confirms that WasUnique and DataTransfer can be active on the snoop response.

Fig 7. A more thorough verification option is to independently develop two similar pieces of VIP and then formally verify them against each other in an equivalence checking exercise. For the ARM ACE protocol, ARM and Jasper engineers independently developed single-interface VIP for ACE (and for AXI) and formally verified the two independently developed pieces of VIP in several back-to-back configurations.

Fig 8. We also test VIPs for correctness. In an example, the cache-coherent interconnect RTL component has two ACE interfaces for connection to master components and three AXI interfaces for connection to slave components. In the verification environment, the VIP models take the place of actual RTL components. In this environment, an ACE system-level VIP is also connected to both ACE interfaces to ensure proper system-level behavior.

Consumer demand for increasing functionality in devices has resulted in multi-core processors requiring more sophisticated cache control. Why? 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 will 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 will demonstrate how to develop and verify system- and interface-level VIP for the ARM ACE protocol.

Cache-Coherent Protocol Specifications     

The first step in creating the protocol is a painstaking approach to developing the protocol specification. Cache-coherent protocol specifications generally define and describe several key elements of the underlying protocol:

• The system components,
• The granularity of coherency, that is, the size of a cache line,
• The access rights that agents have to cache lines, that is, cache-line states,
• The transactions that operate on cache lines,
• The channels or networks the transactions travel on,
• The effect of the transactions on cache-line states, and
• A description of an illustrative subset of the transaction flows in the system.

Cache-Coherent Protocol Verification        

After creating the specification of the protocol, successful verification of the protocol is an equally challenging task. Often, considerable energy goes into the verification of cache-coherent protocols with several forms of verification.

Documenting the protocol is the first form of verification and is effective because it forces careful consideration of various aspects of the protocol on the part of the specification writer. Contemplation of the flows often reveals things that need different handling by the protocol. In addition, creating action tables can highlight holes in the protocol and uncover ambiguities.

Moreover, peer reviews are also very common and naturally occur since there are so many consumers of the specification. The peer-review process often leads to interesting whiteboard discussions that promote clarification from the architect. The architect then incorporates the necessary updates into the specification to remove ambiguities.

The final level of verification is to build a model of the protocol, create high-level properties describing cache coherence, and run simulations against the properties or attempt to prove the properties with a formal verification tool. Note that there are many challenges inherent at this level of verification.

These challenges include:

• Creating a machine-readable specification,
• Ensuring protocol model soundness,
• Debugging the protocol model,
• Verifying the protocol model,
• Using the model for protocol comprehension, and
• Creating a reusable protocol model for RTL verification.