Formal Verification Signoff for Digital IP

At the recent Jasper User Group meeting, one of the presentations was by David Vincenzoni of STMicroelectronics titled Formal Verification Signoff for Digital IP: Can We Use It?

At the risk of revealing the answer to the question prematurely, it turns out that formal signoff is very effective on their digital IP blocks.

The "classical" approach ST uses is UVM-based with constrained-random tests. They improve this a little by adding some formal methodology to help analyze coverage and unreachable code.

The "new" formal-based approach uses the following JasperGold Apps:

• Superlint to find dead code, analyze FSM coverage, overflow, deadlock, and livelock
• CDC to analyze resynchronization schemes
• ABVIP for AMBA compliance
• CSR for register verification
• FPV for functional features
• COV for functional and RTL coverage

A test case was used where there is a finite state machine that implements the power modes on the SoC. There are actually nine modes as you can see in the table above. Two critical signals are power switch enable (PSE), which powers a block down, and isolation enable (ISO) that isolates the block from the rest of the design (and perhaps saves state in retention registers). In a whole cycle of a block being powered up and down, it is crucial that PSE comes on before ISO goes off so that the block remains isolated until power is restored, and correspondingly, the block must be isolated before it is actually powered off.

The FSM was analyzed with simulation, which achieved:

• 95% of FSM block coverage
• 100% of FSM states
• 95% of FSM state transitions
• 100% of SVA assertions related to PSE and ISO signals

But since this block is so critical to the SoC, they decided to run formal verification to prove all the SVA assertions, too. It's a good job they did since they found two bugs, one of which was fatal. In a corner case circumstance, a FSM never switches on PSE but it removes ISO. Formal verification found this in a few minutes.

David compared the classical approach to formal. The classical approach took two weeks of effort plus five weeks for the system application. Formal took two days of effort and found two bugs, one of them fatal, in about two hours. 

As a result, they did some test studies of using formal for IP signoff. The first was a simple controller that they verified with the formal flow, and later a different team verified the IP with the classical flow. I won't go through the details of exactly what they did, but the results were that the formal approach took one week of effort, the classical approach took 12 weeks of effort. The two approaches got essentially the same coverage.

The second case study was a multi-port embedded flash interface and was much more complex. Again, the formal approach took three weeks of effort, the classical approach took eleven weeks of effort.

Formal IP signoff saves significant weeks versus the classical UVM-based approach, as you can see in the image.

This frees up people to be deployed on top-level verification where UVM is still heavily applied.

David's conclusions are that:

• Based on these corner cases caught only by formal, in the future, they will run formal first.
• Formal-based signoff can save significant weeks (12X in the first test case, 3.7X in the second) versus the classical approach.
• They can "easily" apply the formal flow to most of their custom IP.
• From now on, they will use the formal-based flow when it is applicable for IP signoff. Formal verification discovers more bugs in less time than any constrained random test.
• They start the verification phase with cleaned RTL from the Superlint App.
• Dynamic tests are developed for top-level SoC verification.

So, yes, doing formal signoff of IP blocks is a great idea!

 

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