July 7, 2009 -- Everyone is familiar with the old adage about what you get when you assume something—probably not appropriate for print, but there is little doubt of what you are thinking right now. Unfortunately, chip verification is not immune to this adage, and it is in some ways in a precarious situation given the increasing use of formal property checking in verification flows today.

Over the past 10 years there has been significant progress in the area of formal property-checking technologies, making them much easier to adopt and leverage for block and module verification. The advent of standard assertion languages such as Property Specification Language (PSL) and Assertions (SVA), along with increased usability of these technologies, has enabled significant proliferation of use by designers and verification engineers. Data from the Electronic Design Automation Consortium (EDAC) show the year-over-year growth in terms of dollars in the formal property-checking market from 2006 to 2007 as increasing a whopping 47%, compared with simulation over that same period increasing only 12%.

So what does this have to do with assumptions? Assumptions—in technical jargon—are properties written in PSL or SVA. Specifically, they are properties not of the DUT (design under test)) but of the environment around the DUT. And today, assumptions are at the core of how formal property-checking works. By describing the valid behavior of the environment surrounding the DUT, assumptions act to constrain the formal analysis to explore only valid states of the design. What this means then is that the results achieved by a formal run are strictly tied to the validity of the assumptions applied to the formal verification environment. This leaves on the table a huge question: Does the released design in the real world actually obey the assumptions?

By Chris Komar. (Komar is with Cadence Design Systems, Inc.)