AWS and Synopsys have collaborated closely on scaling exercises of EDA workloads on a cloud environment using Synopsys VC Formal next-generation formal verification solution. The solution is designed with a hybrid workflow so that users can start the process on-premises and, once they’ve reached their on-premises compute limitations, they can save their work and resume it on the cloud without having to restart the process. Without any human intervention, the solution can autonomously take advantage of available compute cores, including Amazon EC2 Spot Instances, saving effort on resource management. It also has adaptive machine-learning orchestration capabilities that assigns the most appropriate formal engines to specific verification problems—a feature that runs even more efficiently on the cloud.
AWS provides a suite of cloud solutions; in this blog post, we’ll focus on two that are well suited for EDA flows:
- AWS Graviton2 processors based on the Arm® architecture, which power Amazon EC2 general-purpose (M6g, M6gd, T4g), compute-optimized (C6g, C6gd, C6gn), and memory-optimized (R6, R6gd, X2gd) instances
- Scale-Out Computing on AWS solution (SOCA), which provides deployment and operation of a multiuser environment for computationally intensive workflows
In three different sets of runs, scaling from 12 cores up to 1,200 cores, the two companies tested the VC Formal solution in a SOCA environment on three different configurations:
- AWS Graviton2 processors
- X86 CPU with hyperthreading
- X86 CPU without hyperthreading
Hyperthreading expands the capacity of the system. Without hyperthreading, 16 physical cores maps to 16 CPUs on the system. With hyperthreading, the 16 physical cores become 32 CPUs. The performance delta between the two configurations is typically 10% to 20%. However, the hardware cost can be much higher with more machines. As a custom processor, AWS Graviton2 does not use hyperthreading; instead, every CPU is a physical core.
In the exercises, hyperthreading disabled on the x86 CPU generated faster results but higher costs. With hyperthreading enabled, the performance was in line with that of the AWS Graviton2 processor. However, the big takeaway was, the AWS Graviton2 results demonstrated substantially less cost for comparable runtimes, along with better scaling.
Scaling the VC Formal solution from 12 to 1,200 cores on the AWS Graviton2 processor resulted in a 45x speedup with a 2x increase in compute cost, along with roughly 90% convergence (Figure 1). That’s a shift left in formal verification, from two days to less than an hour.