American humorist and author Erma Bombeck is quoted as saying:
“When your mother asks, ‘Do you want a piece of advice?’ it is a mere formality. It doesn’t matter if you answer yes or no. You’re going to get it anyway.”
As a matter of fact, writing a blog I feel pretty much the same way: I will give my piece of advice whether you reader want or not. And once we’re done with the formalities, I’d like to speak exactly about formalities, or rather – Formal Verification.
And my advice is: you should consider Formal Verification as part of your next ASIC project, along side with Functional Verification.
Some short background for those not familiar with the concept: The most common methodology for verification is functional (dynamic) verification, where we run a series of scenarios through the design and check if the logic behaves correctly in such cases. The good thing is that this should imitate the real life modus operandi of the chip: if it functions flawlessly under such circumstances, it is a good predictor to its real-life performance.
The problem is that it’s often hard to really encompass all the different corner cases the device may operate in: because it’s challenging to scope them, or since it’s hard to document the different modes, or because it will take time to model the verification environment, or yet, because the time it will take to run the different test cases is prohibitive.
Formal Verification addresses the problem from a completely different angle. In this technique, the engineer writes certain assertions that should always (or never) hold true, irrespective of the specific case. Formal Verification tools then go ahead and try to prove mathematically that this is the case.
As a basic example, consider a busy junction with traffic lights. To check the correct functionality of the signaling system you can simulate the pattern by which cars arrive at the junction, at different times of the day, different days of the week, different weather conditions, etc.
In parallel, you may want to validate that any given time (hour/day/weather) there is no more than X open lanes and that they never inter-cross other lanes. And that, at no time all lanes are red, as that will create a traffic blockage.
As you can see, these two methods – the dynamic and the formal/static – are complementary. One models the natural behavior of the system, and the other certifies its holistic integrity.
The fact is that at Veriest, we’ve been increasingly leveraging Formal Verification alongside with Functional Verification, with great results.
From our experience. there are 2 key benefits to Formal Verification.
1) “The earlier, the better”: It’s well known that finding a bug earlier in the design cycle is all goodness: it’s simpler/cheaper to fix such bugs before the circuit gets too complex, the bug gets masked by layers of other functionality, and fixing it may impact other areas of the design. The problem is that in the early days, the functional verification environment may not be ready yet – for reasons mentioned above.
Comparatively, a relatively simple Formal Verification environment can find simple but meaningful mistakes, early on. This approach is compliant with the “shift-left” methodology often used in Agile software development, where an effort is made to find and prevent as many issues as possible early in the process, before they become “hairy”.
In fact, in a paper presented by ARM at a Formal Verification conference documented the following pattern: The same number of bugs were found, but they were found much earlier in the process.
You may notice that the graphs in the bottom of the slide show the usual pattern of bugs finding without Formal (graph on the left) and with Formal (right).
2) Efficiency: Orthogonal to the “shift-left” effect, properly modelling the functional behavior of the circuit in the different scenarios, often requires deep understanding of the system and a sizable investment in people, time and simulation cycles to achieve good coverage.
For certain types of circuits (but definitely not all!), Formal Verification can short-cut and get to comparable coverage with smaller teams. In some projects, it often happens that a Formal Verification team that may represent under 10% of the total team, is responsible for unearthing a much higher proportion of the total bugs in the design (and earlier…).
Elchanan Rappaport, Veriest’s Formal Verification Tech Lead, often compares such techniques to finding if a car tire is punctured. You can start looking for the hole – but this is not at all very efficient; you’d rather sink it in a water basin and just watch the bubbles if something is wrong.
Remember, Formal Verification can’t solve all the verification problems and has its own limitations. So our advice is to use ALL the tools at your disposal – Functional AND Formal Verification – but to use the right tool for the right job!
This week, on October 10-11, Veriest will be attending the Jasper User Group conference in San Jose, CA, one of the major conferences in this field – where Elchanan will be presenting a paper on “A Methodology for Confirming the Safety of Reductions”. Formal experts from companies such as ARM, STMicro, Marvell, HPE, Samsung, Broadcom, Cadence and others will be presenting and discussing their experiences using Formal techniques with other users.