Viewpoint

How Will Anyone Verify Million-Gate Designs?

It is becoming increasingly difficult to verify designs with simulation as gate counts approach the million-gate mark. Formal verification will help fill the gap.

By Allan Wallack

To verify a design is to check that it conforms to a specification. Today, designers try to verify logic by simulating huge numbers of input vectors. They are spending too much time simulating and getting too little verification in return as design complexity grows. Designers are adopting a new approach that augments simulation with faster, more thorough methods that help eliminate two major problems they face when they rely on simulation alone. First, it simply takes too long to simulate all the vectors needed to adequately verify a big design. Second, no matter how many vectors are simulated, it is impossible to ensure that they cover all possible logical input conditions.

Often dubbed "formal verification," the new breed of logic verification tools cuts design cycles by slashing the time designers spend making sure errors don't creep in during the design process. Each verification run is much quicker than simulating a vector set, often by more than an order of magnitude. This kind of verification is inherently complete, eliminating the worry that the vectors will miss a crucial flaw in the implementation.

So what's formal about these tools? Instead of showing how the circuit responds to stimuli, and then relying on the designer to compare the responses produced by two circuit versions, logic verification tools use an RTL or netlist description of a circuit as its specification against which they compare the logic in revised versions. By compiling the two designs into a "formal" representation of the logic, logic verification tools can use mathematical methods to conclusively prove whether the logic in the two versions is equivalent. It is the inherent completeness of these verification methods that causes people to call them formal.

Even as designs pass a million gates, simulation will remain an important part of IC and system design methodologies. Interactive simulation is well-suited to the beginning of the design process, where the initial hardware description language (HDL) model is the design to be verified, and the "specification" exists only in the designer's mind. Detailed timing simulation will remain a crucial step at the end of the process.

But during the middle stages of the design process, simulation is a bottleneck that logic verification tools will eliminate. Instead of having to decide which vectors to simulate and how often to run them, designers will directly compare the logic in their gate-level implementation against the logic in an already verified RTL model. Later, as they refine the implementation--to add test logic, improve timing paths, or fix bugs--they will quickly verify that each new revision is logically the same as the previous version.

Although complete verification is an enormous benefit, it is the need to get products to market sooner that is causing companies to adopt logic verification tools. Use of formal methods is not a guarantee that these tools will save enough time to justify their adoption. But our experience shows that the results can be dramatic: whereas pushing all the vectors through a design with a simulator takes several CPU weeks, logic verification can take just a few hours. That's the kind of improvement that designers need in order to verify million-gate designs.

Allan Wallack is president and chief executive officer of Chrysalis Symbolic Design.

integrated system design  February 1995