The term "verification" today is ambiguous. The more precise use describes an approach employing mathematical methods to assess the hierarchical definition of an IC using techniques that are not directly related to the physical implementation of the circuit. This is also called "formal verification."

The other definition of "verification" is broader and synonymous with validation -- that is, making sure your IC design works correctly and does what you want it to. In this context, verification embraces the whole arsenal of techniques, including mathematical proofs of formal verification and simulation, that engineers traditionally use to convince themselves that their design works as it should.

The addition of formal verification to the chip designers' arsenal reflects the rise in chip complexity. When design complexity increases, it is tough to prove with simulation that the chip will work under all conditions, primarily because it is difficult to envision and simulate all the combinations of events that may lead to problems.

With more complex designs, simulation still has a role, but heavier guns are needed for full verification techniques. Formal verification is a relatively new field with few commercial tools available.

To begin, you must determine parts of the design that can be handled by available formal verification tools. If there's a match, these tools will cut back dramatically on development time.

For example, if you're trying to check the equivalence between a hierarchical description and a gate- or a transistor-level description, formal verification knows how to do that well. In contrast, simulation seems to take forever and can be incomplete. Alternatively, if you're trying to check more complex design properties -- for example, to see if your design will always respond to a request and won't deadlock -- those evaluations are more difficult to handle.

Once you've determined the appropriate sections for formal verification, it requires work that is more intellect intensive, yet less time intensive than simulation. In many cases, formal verification requires specially trained people who understand how to apply the mathematical techniques to verify the design.

In other words, the cost in moving from one approach to the other is in the training. Design engineers must learn how to approach verification with a layered model of the system in mind. Bridging the education gap between what engineers know and what they need to know to use verification effectively is a serious issue. The training is not available today in universities and chip design companies don't want to focus on it because they don't consider training as crucial to completing the design.

EDA companies are also in a tight position regarding training. If they develop tools that require significant training, customers are less likely to support them because of the training cost. Customers are also wary because many formal verification tools require the design process to be altered.

On a more positive note, as verification begins to mature, we are beginning to see standardization. There is now some standardization in equivalence checking, which validates that the hierarchical description for the synthesis tool matches the final design at the gate or transistor level.

But at higher levels, where you're trying to check other parts of design correctness, there is still disagreement about how to accomplish that properly. A formal technique called "model checking" holds a lot of promise there.

While model checking has been around for a while, applying it requires a mathematical background -- again the training issue. Users are required to specify properties in a formal mathematical way that requires a significant jump in education and a change in vocabulary for design engineers.

At this year's DAC, June 18-22 in Las Vegas, we will look at the advances in formal verification and seek to understand how all of this comes together to solve the problems at hand.