Dyjm353IByLH (Gast)
| | Hi, Neil. Let me preface this comnmet by stating that I represent a formal verification company, Jasper Design Automation.This is a very interesting discussion. It captures a trend we are seeing among many of our customers in which verification is driven back upstream into the design process. The nature of formal makes it extremely effective at catching bugs early, and for unit level testing it has proven very effective. A single property can go a long way towards helping a designer flush out bugs or better yet, avoid inserting them in the first place.Mike Bartley of TVS wrote a great vendor-agnostic paper about the pros and cons of formal deployment. I don't see it on their website, but it's a very good insight into how leading-edge formal users such as ARM are deploying Jasper. One of the most interesting aspects of the paper is defining a taxonomy of formal deployment. What they propose is:Bug Avoidance (designers using formal to eliminate bugs and reduce spec ambiguity)Bug Hunting (systematic use of properties to uncover bugs at system/subsystem level)Bug Absence (full proofs of critical behaviour at system/subsystem level)Bug Analysis (isolating and verifying foxes for late-phase corner-case bugs)The bug avoidance deployment model is very close to what you describe, and has a very rapid RoI. And, yes, we would assert (ahem) that Jasper's technology ameliorates many of the historic drawbacks of formal methods. |
