Using Formal to Find Bugs in ARM Microprocessors

2.5x ROI vs simulation. 25% of bugs found for only 10% of the overall verification cost. 36% of bugs in a current CPU project. These impressive results for formal analysis are what ARM’s Laurent Arditi reported at JUG 2013 after painstaking recording of metrics over several production programs.

As you can see from the above graph, adoption has gone in a two steps forward one step back way but now seems to be on track to increasingly wide adoption. This has been because of a perceived lack of ROI on the investment in tools and training in the early years. So Laurent’s approach is two fold:

• demonstrate that common statements about formal verification (it is limited in size, can’t handle the designs we do, doesn’t find real bugs) are false
• show that there are approaches that drive down verification cost (of formal and simulation) and increase the benefits

So what are the aspects of a design to focus on:

• embedded assertions/properties are primarily written for simulation and so can be used for formal at no extra cost
• X-propagation is low hanging fruit since simulation has issues with it and formal can do it with very few hand-written properties
• complex clocking schemes are hard to verify with simulation but formal has found many corner case bugs and a major bug on the Cortex-A12
• use Jasper ProofKits
• reduce the cost of simulation. correlate formal coverage with simulation coverage, don’t try and do stuff like X-propagation in simulation, remove a big effort from simulation/humans
• use simulation tricks (like reducing FIFO depths, changing arbitration) to reduce formal proof times too

The Cortex-A12 had a lot of use of formal. It accounts for less than 10% of the verification costs and found 18% of the real bugs (maybe even 25%). So ROI for formal is 2.5X compared to simulation. On another (unidentified) CPU in development, 36% of all bugs were caught by formal (see the graph above).

Another phenomenon is that with enough simulation most bugs get found anyway, but with formal they are found much earlier, meaning less RTL churning, especially late in the design cycle when it is hard to cope with. This is partially because formal can start before simulation testbenches are ready.

How do you discuss formal with managers? Firstly, don’t raise expectations that nothing happens and suddenly the entire design is formally proven, that’s just not the way the world is (and probably will never be). Don’t forget that although you may care about what is proven, managers do not. Highlight how the coverage is increasing and the number of problems found. Finding bugs early saves a lot of simulation time, and found late shows how formal finds corner cases that simulation misses.

There is more in the presentation. If you are a Jasper user (not necessarily one who attended JUG) then you can download the presentations, including this one, here.

More articles by Paul McLellan…