An InFormal Chat

Any sufficiently advanced technology is indistinguishable from magic, as the saying goes. Which is all very well when the purpose is entertainment or serving the arcane skills of a select priesthood, but it’s not a good way to grow a market. Then you want to dispel the magic aura, make the basic mechanics more accessible to a wider audience and push usage/applications rather than the mystical spells of the inner circle. After all, few of us have a deep understanding of how our smartphones work but now they’re used by virtually everyone.

Some of what this takes is usability – we engineers never met a problem we believed couldn’t be solved by yet more engineering, in this case through better user experiences, more attuned to the way we think and even the way we communicate (touch, gestures, speech, …). But in some cases, widespread adoption also depends heavily on socializing the domain. Or, back on the magic analogy, showing how the trick is done – not professional magician to professional magician in magician-speak, but simply explained to us non-experts who just need to make the trick work to get our jobs done, along with a basic understanding of what happened behind the curtain (or inside the hat).

Formal verification fits this description all too well. We know it does incredible things, providing complete proofs inaccessible to dynamic verification, but much of what is written about the domain today is expert to expert, full of math and strange terms like witness and bounded model-checking. Usage in some areas has been simplified but we still wonder how those kinds of verification fit into our overall test and coverage objectives. And other areas still look inaccessible to anyone but PhD experts who must understand bounded proofs, BDD versus ATPG versus SAT and how to mutter all the right incantations to sufficiently constrain (but not over-constrain) their proofs.

All of which makes it very timely that Synopsys is launching a blog today called InFormal Chat, written by verification engineers for verification engineers. I’ve read some of the initial blogs. They’re informal and short, each a quick read to pull back the curtain on some aspect of formal verification. They don’t worry much about polished delivery – this is engineers talking to engineers with little marketing interference.

Synopsys is clearly proud of the expertise they have built up in the VC Formal team, and in the product, and want to get the message out that they are a leading contender in this area. They’ll talk certainly about tool capabilities but they also want to help users and potential users better understand the magic. Some of the discussion will be on the mechanics of getting though formal analysis, like how to handle incomplete proofs and where to watch out for pitfalls. They’ll talk sometimes about advanced topics, such as how to build proofs for cache-coherency. And they are committed to providing thought leadership in the domain, in emerging problem domains and suggested solution approaches.

This is a worthy direction to socialize formal verification and to convert more of us to being at least passable formal magicians. I’m told new posts should appear every couple of weeks. Together with a good search mechanism, this should be a valuable resource for all of us formal wannabees. You can find the link HERE.