Get email delivery of the Cadence blog featured here
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:
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:
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:
So, yes, doing formal signoff of IP blocks is a great idea!
Sign up for Sunday Brunch, the weekly Breakfast Bytes email.