Proof engines are vital to SoC flows

Proof engines are vital to SoC flows
By Ron Wilson, EEdesign
October 11, 2002 (3:28 p.m. EST)
URL: http://www.eetimes.com/story/OEG20021011S0038

As verification's role in system-on-chip design flows keeps growing, more industry resources are being dedicated to stemming the expansion. It is not a coincidence that most of the rapid growth in EDA this year has been among verification tool suppliers.

Along with the sheer proliferation in tools has come increasing sophistication in techniques. The old notion of throwing functional test vectors at a design until the schedule is used up has become a formula for failure. In its place have come numerous ideas for simplifying and rationalizing the problem: partitioning the chip into smaller verification problems, building reusable test benches and shifting to assertion-based approaches.

Within this latter trend, there are several different ways to use assertions. The assertions may be simply rules coupled with checkers that define the critical parts of a protocol, or at least the parts that the designer hopes are the critical ones. These checks ar e conducted during traditional vector-driven simulation runs to verify that, whatever else it might do, the design at least isn't screwing up the bus protocol.

But another use of assertions is appearing as well. This use is sort of a second wave of the formal verification movement. It is possible to use formal reasoning techniques to prove for which set of inputs a given assertion is true or false for a given design. This, for example, can be used to prove that there is no set of inputs that will cause an adder to produce the wrong output. Or it can be used to determine the exact combination of inputs for which the output will be correct.

Expanded range

Clever devices permit such tools to be used for sequential machines as well as for combinatorial logic. This extends the range of formal assertion proving to, for example, state-machine controllers and bus interfaces.

These capabilities considerably expand the range of formal proof engines beyond their original use in equivalence checki ng. It is probably fair to say that many design teams now use equivalence checking at some-or all-points in their flow in which the design has undergone a transformation. But assertion checking gets at a more fundamental question: Was the design right in the first place?

Clearly the value of the new tools hinges on some key assumptions. One of these is that the desired and forbidden behaviors of the design are completely captured in the assertions-not a trivial statement at all. Another is that languages exist for capturing assertions sufficiently standardized and robust to be practical for everyday use. A third is that the proof tools themselves can be either sufficiently obvious or sufficiently documented that nonmathematicians can use them productively.

None of these assumptions is exactly a given at the moment. Most system designers are not used to specifying their intent in terms of assertions, and few are interested in creating two parallel designs: one a behavioral model in C or some modeling language, and the other a formal specification in some assertion language. The languages themselves are a matter of considerable debate. And the tools are still emerging.

The one thing that can help in such an unsettled environment is information. One technical paper by Arne Boravl of Prover Technology (Stockholm, Sweden) contributes to that cause with an excellent beginning tutorial on the subject.