JAWS: JasperGold in the AWS Cloud

At the CadenceCONNECT Jasper User Group meeting in December, one of the presentations was by Richard Paw of AWS on a Cadence/AWS project called JAWS, for JasperGold on AWS. I covered it in the second half of my presentation Jasper User Group: The State of Formal in 2020.

Now Ahmed Elzeftaw and Mike Pedneau have written a much longer blog post on the AWS for Industries blog, going into a lot more detail with a focus how you can learn from their experience.

The summary paragraph of the project says:

In order to explore how semiconductor customers can utilize the scale and flexibility of AWS Cloud for design verification, Cadence and AWS launched this joint investigation to examine the benefits of scaling-up the JasperGold® Formal Verification Platform on AWS to a scale that customers can achieve on their own. We used the Scale-Out Computing on AWS solution (SOCA) to scale-up the JasperGold workloads to 960 cores.

The AWS/Cadence team picked using JasperGold to do some of the formal verification for a Tensilica processor...although I don't think there was anything special about that choice, just that, as Cadence, we have lots of Tensilica processors and other big digital designs not so much.

The blog post continues:

Depending on the nature of the verification task and method, the time to complete verification can be reduced by splitting the verification workload into multiple tasks, which can be run in parallel. Any verification tests which are in themselves independent of other tests can be run in parallel, reducing overall time to complete with no reduction in verification quality. Formal verification can benefit particularly well from such parallelism since a formal test bench for these complex designs typically consists of thousands of properties, or assertions, which can easily be analyzed in parallel by today’s leading tools such as JasperGold.

The "control" for the experiment was an on-premises (on-prem) server with 12 cores. Something realistic that a verification team might have access to.

There is a lot of detail that went into these numbers about the types of jobs, but the bottom line was that they got a speedup of 5.5X with 96 cores, and of 20X with 960 cores. If your first thought is that these numbers are very disappointing, as mine was, don't forget that the baseline is 12 cores. So they get a 5.5X speedup with eight times as many cores, which is much better both in terms of linearity and cost of the cores.

Another money quote:

We ran the fourth iteration on the 960-core configuration only, due to time constraints. This iteration found new useful proofs, including 23 with cycle bounds large enough to be valuable, and importantly, found four deep security bugs.

Presumably, those same issues would have come to light using the on-prem setup...which they estimate would have taken five days to complete, instead of a bit over four hours.

There is a lot more detail in the white paper about what kinds of queues to use, which I won't go into here. But if you are a formal verification engineer, especially someone looking at using AWS, you should definitely read the white paper.

Learn More

The AWS blog is Running Cadence JasperGold Formal Verification on AWS at Scale

Here is the JasperGold Product Page.

Sign up for Sunday Brunch, the weekly Breakfast Bytes email.