Verification Test Plan: The Book
Missed the movie? Here's the book!
I don't know about you, but I had a time conflict on the morning of Thursday, July 27th, and hence couldn't attend one of the key panel discussions that took place that day in San Francisco at the 2006 Design Automation Conference in Moscone Center.
This not-to-be-missed panel showcased several of the leading gods of verification, and their friends, as they discussed issues related to the building of a verification test plan.
If you missed the event, as I did - or even if you were there - this is your lucky day, because herein you will find an improved version of that panel discussion. It's improved because:
A)You can read it at your leisure, hopefully with a good cup of coffee in hand;
B)There are several additional participants here who did not appear on the original DAC panel in July, but who have contributed substantive comments to the discussion below;
C)The book is always way better than the movie - more detailed, more complex, and with greater nuance.
So keeping these thoughts in mind, please read on. We're delving into a host of topics here, among them being formal verification, emulation and simulation, the division of labor between the design engineer and the verification engineer, and how to knit the whole darn thing together. Pretty interesting stuff!
Building a Verification Test Plan: The Book
Alan Hu - Department of Computer Science, The University of British Columbia
Andy Piziali - Verification Application Specialist, Cadence Design Systems
Craig Cochran - Vice President of Marketing, Jasper Design Automation
Catherine Ahlschlager - Hardware Manager, Formal Technologies Group, Sun
Doron Stein - Hardware & CAD Engineer, Cisco Systems
Harry Foster - Principle Engineer, Mentor Graphics
Janick Bergeron - Scientist, Verification Group, Synopsys
Rajeev Ranjan - CTO, Jasper Design Automation
Rich Faris - Vice President of Marketing & Business Development, Real Intent
Chapter I - Some Background
1) Please define formal verification.
Alan Hu - Formal verification means proving a property about a model of a system. "Proving" is in the sense of mathematical proof - the highest level of confidence of anything known to humanity. In other words, you have 100% coverage of all possible behaviors of your (model of your) system.
"Property" means you have to specify what you're proving, and this is the same problem whether you're working with formal or informal verification. If you don't know what you want (you don't specify to look for a particular case), you won't know to verify it. And "model" means you're always verifying something other than the actual product in the customer's hands. The model could be the layout, it could be gates, it could be a very abstract protocol, or an algorithm.
2) Please distinguish between an assertion and a property.
Alan Hu - I don't. Keep in mind that I'm speaking with the luxury of being an academic. In different contexts, some communities may draw a distinction.
For example, some people will say that "assertions" are embedded in the design, whereas "properties" are external to it. Other people will have other definitions. I don't think any usage has become the de facto standard, so if I'm talking to someone, I'll just keep listening until I figure out what distinction they're really trying to make.
3) At what point did formal verification become more than an "academic curiosity?"
Alan Hu - What we're seeing is a gradual process, and it's hard to cite a defining moment. Even thirty years ago, for certain niche markets, formal verification was already being used. Twenty years ago, companies like IBM had started doing formal equivalence verification in-house. Ten years ago, formal equivalence checking was taking over the RTL-to-gate market, and the big semiconductor and EDA companies (Intel, IBM, Cadence, Synopsys, etc.) and several start-ups were all ramping up on model checking.
Today, the model-checking (or property-checking) tools are gaining market traction, and RTL-to-gate equivalence checking is so completely owned by formal tools that most people don't think of it as formal verification anymore. Ten years from now, even more formal techniques will be mainstream parts of the design flow, but some formal verification problems will still be in the realm of academic research. It's important not to keep redefining formal verification to mean whatever we can't quite do yet.
4) Is it possible to verify a large SOC without using some form of formal verification?
Alan Hu - Sure. You can carefully hand-pick exceptionally good design and verification engineers, choose an extremely conservative (i.e., low performance) architecture and design that's "obviously correct," buy a ton of emulation boxes and server farms, simulate for a really, really long time, and do some extra spins of silicon until you get most of the bugs out.
The real question is whether it's cost-effective to do a large SOC without using some form of formal verification. And I'd have to say the answer is no. People vote with their wallets. Everyone these days is using formal for verifying RTL-to-gate equivalence, for example. People have decided that's the most cost-effective way to do that step.
For property checking, the value proposition is less clear. All of the people doing the most complex chips - the microprocessors and GPUs and very complex SOCs - are all either buying or developing in-house formal property checking tools. In some cases, they are developing extremely sophisticated formal methodologies, as well.
So, on the leading edge, the value proposition is definitely there. For the trailing-edge designs, though, people apparently can get by with older technology for a bit longer.
Chapter II - The Panel Discussion
1) What is a verification test plan (a spreadsheet, a GUI, a document?) and how does it differ from traditional verification strategies?
Harry Foster - Verification planning is not a thing - it is a critical process of design. Some might view this process as a means to an end (that is, a written document or verification feature checklist), but it is so much more than that. It is a fundamental component of the design process, and its analysis component often uncovers design and architectural bugs prior to implementation or application of any form of verification!
Janick Bergeron - A verification plan is a list of features of the design that need to be verified. A verification plan could come in many forms, such as a spreadsheet, a document in natural language, or it could simply reside in the engineer's head. The industry hasn't yet settled on the best approach to define a verification plan.
Doron Stein - A verification test plan should be a combination of a database (hence a dynamic infrastructure) with the ability to produce a "traditional" test plan in a document form or an HTML format. By establishing such a structure, we encapsulate the ability to reflect correct status with in the verification plan thus closing a bit the verification loop (plan, execute, evaluate your planing, execute, etc.).
Catherine Ahlschlager - Most of the test plans that I've seen are documents that describe the overall verification strategy, and features to be tested and how to test them. They are often translated into spreadsheets, so that coverage/tests can be written to monitor how the project is doing against the schedule. In addition, milestones are usually included to outline deliverables on each verification phase.