An Informal Update

I mentioned back in June that Synopsys had launched a blog on formal verification, intended to demystify the field and provide help in understanding key concepts. It’s been a few months, time to check in on some of their more recent posts.

First up, it feels like they are finding their groove. Relaxed style, useful topics but now with a little more polish. Not marketing polish (heaven forbid), just good, sometimes even witty writing style. That makes these blogs (running now at about 2 per month) fun to read, which in turn should make them all the more effective in helping us become comfortable and more knowledgeable about the domain. Following is a quick (and incomplete) summary of a few that caught my eye.

Iain Singleton (a fellow Brit) blogged on abstractions and why we should feel perfectly comfortable with this idea. In formal it is often necessary to replace a complex block of logic with a simplified FSM, modeling just the interesting corner behaviors of that block for the purposes of the current verification objective. Iain draws a parallel with his support commutes (in England) from Lancashire to the South East. He relates something every commuter will instantly understand – sometimes you look up and don’t know where you are or how to get where you are going. Yet you continue on auto-pilot without missing a beat. You can do that because you have subconsciously abstracted the route. Your brain doesn’t worry about intermediate details, it just remembers the principal milestones. Which is exactly what you are doing when you build an abstraction for a formal proof.

Abhishek Muchandikar wrote a blog on how to develop confidence that you can signoff in the presence of inconclusive proofs, an important question many ask about formal. Abhishek uses another analogy I like – the (ancient) Greek phalanx formation (don’t you love it when engineers undermine the nerd myth by both knowing this stuff and using it in their writing). The phalanx formation was designed to be close to impenetrable and unstoppable, but naturally was no stronger than its weakest soldier. A similar concept applies to formal signoff in the presence of inconclusives (bounded proofs). For these cases you can run a bounded coverage analysis to the same depth to understand what parts of the code were not reached in this bounded proof, and what constraints (if any) may have limited reachability. All bounded proofs will have a weakest soldier, but adequate analysis on that weakness can lead you to confidently assert that the weakness is acceptable.

Anders Nordstrom posted a blog on a couple of exotic usages for formal, taken from this year’s DAC. One was on hardware/software co-verification using formal methods. I was able to find an open link to the first paper he names but not the second. The first method uses specialized formal tools which can do formal proving in both RTL and C, so is perhaps a little out of reach of most of us. However, I could imagine you might in some cases model the software through an (RTL FSM) abstraction which could then be included in the hardware proof. The second exotic application Anders mentions is formal verification of mixed signal designs. There’s in fact a fairly rich list of papers around this domain. TI presented a paper at DAC on using abstract models for interface blocks in applying formal methods to verify interface behavior.

I’ll wrap up with one more blog, from Sean Safarpour, on the organic growth of formal verification. This is interesting in part to understand where formal adoption is growing but in some ways even more to understand how that is happening. Sean said that in previous trips to Asia he found that he was pushing formal, interest was high but progress between visits was limited. The climate was completely different on his most recent trip; he didn’t have to pitch, customers were now pitching him on their successes in using formal and how they now need help to further expand usage.

Sean makes some interesting points on how this happened. The myth that formal requires deep formal expertise still persists, yet Sean says that there are probably only a dozen or so such people in Asia. Hiring more expertise is therefore not a practical solution to expanding usage. Instead expertise has to be grown organically, yet companies can’t afford to wait for years for engineers to become deep experts. Instead they are seeding interest in verification groups (through conference attendance for example), encouraging a champion, growing a pilot group around that champion, starting with the simpler formal applications (apps) and socializing successes within engineering and also up the management chain. I suspect many other successful adoptions started in the same way. Good input for those of you still on the fence.

You can access the full set of blogs HERE.