Cache-Coherence Verification

As consumers, we place many demands on our personal electronics, especially mobile devices. We want them to perform all sorts of tasks efficiently, accurately, and with minimal power consumption. Complex embedded SoCs have largely enabled the functional capabilities of these devices. To ensure that these devices perform at a desired level to accomplish the tasks needed, today’s embedded SoCs must consist of high-performance, heterogeneous, and multi-processing agents. The presence of a large number of data processing agents sharing a memory resource on an 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.

At its core, cache coherence means the following:
* A read to a coherent memory location reads the data that was last written to the same memory location. For example, a read to location X that follows a write to location X with value D must read the value D provided that no other writes to location X occur before the read.
* Writes to the same coherent memory location are observed in the same order by all components in the system. For example, if memory location X has been written to with values D1 and then D2 by one or more agents, then no agent must ever observe D2 and then D1.

One recent, and particularly complex, implementation of a cache coherence protocol is the ARM AMBA® AXI Coherency Extensions (ACE™) protocol. Since ARM provides the specification, rather than pre-verified blocks, it was necessary to develop Verification IP (VIP) in support of this new product. Using newly-developed ActiveModel™ technology, Jasper Design Automation and ARM successfully collaborated on a project that developed and verified system- and interface-level VIP for the ACE™ protocol. Cache-Coherent Protocol Specification

Cache-coherent protocol specifications generally define and describe several key elements of the underlying protocol, including the following:

* System components
* Granularity of coherency, that is, the size of a cache line
* Access rights that agents have to cache lines, that is, cache-line states
* Transactions that operate on cache lines
* Channels or networks the transactions travel on
* Effect of the transactions on cache-line states
* Description of an illustrative subset of the transaction flows in the system

After creating the protocol specification, an equally challenging task is to sufficiently verify it. Often, considerable time and energy goes into the verification of cache-coherent protocols with several forms of verification needed.

The verification of the protocol usually begins with a documentation process. For the ARM ACE protocol, the Jasper ActiveModel table-based entry format was used to create an executable model. As seen in Figure 1, the format is similar to the entry format used by many cache-coherent protocol specifications where the current state and input activity are shown in columns on the left-hand side of the table (green) and the next-state transitions and other activity are shown in columns on the right-hand side of the table (yellow). The rows of the tables represent the various possible combinations of input activity and current state followed by the appropriate actions for each combination. These ActiveModel tables can be used in place of the tables the architects write, which eliminates one potential source of errors.

Next, ensuring protocol model soundness is vital. In the case of the ARM ACE, this included knowing whether the model could get into all the possible states that should be searched. Like a typical coverage-driven verification flow of an RTL design, coverage points were automatically instrumented into the protocol model to ensure that interesting states were being explored. Using Jasper ActiveModel in conjunction with the tables created for it (and for the documentation phase of the verification), we were able to determine which covers could not be reached where the protocol was over-specifying cases that weren’t possible. Removing the over-specified cases added clarity to the specification. We were then able to use the same technology to automatically generate a full check to ensure that at least one row of the table is always being referenced. This check identified holes in the specification indicating that the specification needed to be re-examined and modified accordingly.

Figure 1: Table-driven creation of an executable model.

During the protocol model debugging phase, we realized that debugging a cache-coherent protocol model is typically not much different than debugging any RTL-based design. However, there were a few things that we recognized as unique and useful. During typical RTL debugging, when a checker fails, a waveform showing the failure is produced, and a normal flow of tracing back from the failure ensues and continues until the bug is found. This process is usually adequate, but it has room for improvement. For example, it was beneficial to have a high-level view of the events with a link back from the property failure to the relevant tables in the specification. This gave us a better idea of what was and was not occurring (Figure 2).

Figure 2: A high-level view of a checker failure.

In addition, debugging protocol model failures is difficult because many transactions occur in parallel and the combined behavior sets up a sequence that violates the check (Figure 3a). Eliminating unimportant transactions from the waveform reduces the amount of information the user has to process and helps to speed up debugging time (Figure 3b).

Figure 3a: The full transaction report.

Figure 3b: The filtered transaction report.

Cache-Coherent Protocol Verification

A cache-coherent protocol specification describes the rules that, when followed, keep the caches in the system coherent. These rules are the assumptions made about the operations of the components of the system. Recall that high-level cache coherence means a read to a coherent memory location reads the data that was last written to the same memory location, provided no other writes occur. Also, all agents must observe writes to a coherent memory location in the same order. These statements were constructed as high-level properties (assertions) and then verified against these protocol specification rules (captured as assumptions).

The formal verification process of the ACE ActiveModel-based protocol model proved to be effective at both clarifying the specification and ensuring the correctness of the protocol model, which was later used to verify the RTL. The challenge in using the protocol model to verify the RTL is in mapping the abstract protocol model states and transactions to the corresponding RTL states and transactions. This challenge is compounded by the fact that the RTL is constantly changing and thus potentially breaking the map. To deal with these challenges, the protocol model was created with protocol rules written at the interface level. By doing this, the RTL is able to connect directly to the protocol model, which bypasses the need for mapping. The ACE ActiveModel became the system-level VIP used to verify the RTL. The protocol rules that came out of this process can be used as assertions (checks) when the model is attached to the RTL. These assertions/checks verify that the RTL is cache coherent.

Summary

Cache-coherent protocols and the RTL implementations of the components of the protocols provide unique verification challenges. Initially, the protocol must be modeled and verified to demonstrate that it adheres to high-level, cache-coherence rules. A large audience, such as RTL designers and verifiers, must also understand the protocol. To enable high-quality verification of RTL protocol components, a sound methodology is imperative when developing VIP for the protocol.

The work that Jasper Design Automation and ARM did to verify the ARM cache -coherent protocol and RTL implementations can be used as a benchmark for cache-coherence verification. The ACE protocol was effectively modeled and verified. The model also served as a platform for querying the protocol to understand transaction flows and freedoms in the protocol. In summary, the ACE ActiveModel model along with the ACE interface-level VIP stand to play a critical role in the eco-system of AMBA4-based SoC design and verification.


Rajeev Ranjan is CTO of Jasper Design Automation.

for a copy of a full Jasper white paper on cache coherency verification, click here