Formal Verification at ARM

There are two primary microprocessor companies in the world these days: Intel and ARM. Of course there are many others but Intel is dominant on the PC desktop (including Macs) and ARM is dominant in mobile (including tablets).

One of the keynotes at last month’s Jasper User Group (JUG, not the greatest of acronyms) was by Bob Bentley of Intel, talking about how they gradually introduced formal approaches after the highly visible and highly embarrassing floating point bug in 1997. I already blogged about that here. Bob took time to emphasize that Intel doesn’t endorse vendors and so nothing he said should be taken as an endorsement of anyone. He did say that beside using commercial tools they also have some of their own internal formal tools.

Later in the day ARM talked about their use of formal verification and, in particular, Jasper. Laurent Arditii of the ARM Processor Division in Sophia Antipolis (where I lived for 6 years, highly recommended as great mix of high tech, great lifestyle and great weather) presented. In some ways this was an update since ARM presented on how they were gradually using more and more formal at last years JUG.

He characterized ARM’s use of Jasper as AAHAA. This stands for:

• Architecture
• bug Avoidance
• bug Hunting
• bug Absence
• bug Analysis

Architecture:
Specify architectures using formal methods and verify them for completeness and correctness. For example, ARM used this approach for verifying their latest memory bus protocols. They talked about this at last years JUG.

Bug Avoidance:
Catch bugs early, during design bringup, usually before simulation testbench is ready. By catching bugs early they are easier and cheaper to fix.

Bug Hunting:
Find bugs at the block and system level. Server farm friendly (lots of runs needed).

Bug Absence:
Prove critical properties of the design. This is complex expert stuff and requires considerable user-expertise.

Bug Analysis:
Investigate late-cycle bugs. Isolate corner-case bugs observed in the field or in the lab. Confirm the correctness of any fixes.

Jasper formal is now going mainstream in ARM, which is a big advance from last year when it was starting to get traction in just some groups. Bug Avoidance and Hunting flows are leading the proliferation and give an early return on investment. They now have formal regression flows running on their server farm. Formal is no longer a niche topic. At an internal ARM conference on verification they had over 100 engineers interested. Just like Intel, a lot of the introduction of formal requires cookbooks and flows to be put together by real formal experts and then proliferated to all the various design teams.

For example, the above graphic shows two IP blocks. One was done with classical techniques (aka simulation). The other, an especially hard block to verify, was done using formal techniques with no bringup testbenches. As you can see, most of the bugs were found much earlier.

Currently Jasper is heavily used for various aspects of AAHAA. You can see in the above diagram how Jasper features map onto the AAHAA taxonomy.

In the future, apart from propagating additional formal techniques, ARM wants to use formal approaches for coverage analysis, IP-XACT validation, security validation (TrustZone), UPF/CPF (power policy) in formal