Complex IP such as the GPUs or CPU cores designed at Arm consist of many lines of Verilog code, written by teams of hardware engineers over many months. Even so, they must be bug free when they are delivered to our customers. The cost of making a batch of chips using the latest process technologies is astronomical, and so bugs have to be eliminated before we release a product.
The process of looking for errors in designs is called verification, and it has traditionally been market lead by simulators such as Cadence’s Xcelium, Siemens’ QuestaSim and Synopsys’ VCS. These work by creating a virtual model of the design and examining what happens as the clock steps forward while applying a set of external stimuli to the design’s inputs. The simulations can be very comprehensive, allowing our verification engineers to even simulate an operating system booting on a new core, albeit very slowly.
Verification engineers write testbenches that model the behavior of components that would interact with the design under test. For example, they might write a software model of the memory system that the simulated core can interact with. This would capture any deviations from the expected performance as the simulation runs.
Formal verification is an approach to show the correctness of designs that is becoming increasingly popular as it can catch bugs that might be missed by traditional methods. Formal verification tools, such as Cadence’s JasperGold, aim to prove whether statements (properties) written by the verification engineer will always hold true. And they examine the full state space of the design under test rather than only a specific stimulus.
Arm has been using formal verification for some time, and has been a pioneer in our move to running our engineering workloads on Arm architecture servers. The Cortex M55 project was the first to uncover design bugs using Arm servers, running JasperGold. The project’s switch to running on Arm was trivial, and was soon followed by many other projects who took advantage of our on-premise cluster of Arm nodes.
Formal verification did not form part of our first phase of migration into the cloud, so we have not previously talked about the performance of JasperGold on AWS Graviton2. With the recent launch of AWS’ X2gd instance type, combining a Graviton2 processor with 1TB RAM, enabling our formal workflows to run in the cloud has become even more interesting.
In preparation for such a migration, we have recently run an analysis of the performance of JasperGold on Graviton2, compared to the previous generation instances that are available in AWS.
We took a CPU testbench designed to run in our on-premises cluster and modified it so we could evaluate performance when executed on a single instance in AWS rather than tens of machines in our datacenter. We ran the same testbench multiple times to account for any noise in our results, and we looked at two pairs of instance types in AWS.
The machine pairs we tested were the x2gd.16xlarge compared to the x1.16xlarge, and the r6g.16xlarge compared to the r5.24xlarge. In both cases, we are comparing the Graviton2 with the previous generation x86 in that instance family type. We reviewed both x class and r class because the r5 uses a more modern CPU than the X1. So we were interested to see the relative performance for both, given that not all proofs will have such large memory footprints.
We found that the x2gd completed our test suite 33% faster than the x1, leading to a cost per run that was 47% less expensive at list, on-demand prices. While the r5 finished 18% faster than the r6g, it also has 96 cores compared to the Graviton2’s 64. This resulted in the overall test costing 35% less on the r6g than on the r5, while also using fewer licenses.
We are now well into the process of enabling our engineers to run formal verification jobs in the cloud and look forward to seeing the productivity gains they will realize.
Explore EDA on Arm
This is excellently written. Amazing!