SAN FRANCISCO — If further proof was needed to demonstrate that logic verification is becoming a major bottleneck in today's design flows, you should have tried to squeeze into two packed technical sessions that addressed formal verification at the 35th Design Automation Conference.

A user panel was assembled to address issues of formal verification, and a second session of presentations addressed bridging the gap between simulation and formal verification. Both revealed that formal verification is expanding in definition as well as in popularity.

In the user panel, Michael Payer, project high-level design flow senior manager at Siemens AG Semiconductors (Munich), said 46 percent of Siemens' total ASIC development time is currently consumed by verification, and that problems are sure to grow with expanding gate counts.

Participants in both sessions said that simulation and emulation, the tools traditionally used to find bugs in a design, are not finding the corner case or hard-to-find bugs that can occur hundreds of thousands of cycles into a design, and are well beyond the reach of conventional simulation and emulation technologies.

To find corner case bugs, many verification engineers are now seriously checking out formal verification tools. The demand is fueling a huge effort from EDA companies to crank out formal verification solutions, and is expanding the verification tools space to include new technologies that find bugs where simulation and even formal verification fail.

In back-to-back presentations, David Dill, cofounder of verification start-up 0-In Design Automation (San Jose, Calif.) and a professor at Stanford University, and Ken McMillian of Cadence Design Systems, discussed technologies and methodologies for bridging the gap between simulation and formal verification.

"Simulation and emulation, the conventional techniques that are available to us, are not really keeping up with the trends in design," Dill said. "A lot of people hope that formal verification will come in and solve the problem, but unfortunately it is false. I think it will make a valuable contribution but it will not solve the whole problem in the time frame we would like to have it solved, but there are some neat alternatives."

Dill defines formal verification as "anything that ensures consistency with the specification for all possible inputs." He includes equivalence checkers, model checkers and theorem-proving tools in the category of formal verification tools, and classifies another group of what he calls "semi-formal verification tools" as those that bridge the gap between simulation and formal verification.

"Semi-formal verification will be the workhorse for eliminating late-stage bugs in RTL," he said.

Dill proposed coverage measurement as one way to address the gap. The philosophy of coverage measurement, he said, is to quantify the coverage of the test. Engineers quantify coverage in a mathematical way, build tools that analyze and report on coverage, then use those results to optimize the test for the testbench. They can then choose to run simulation or otherwise add more tests based on the measurements.

Code-coverage tools are another semi-formal solution. Dill said these tools find bugs and cover large designs, but do not solve the entire problem.

Yet another technology in this area is design fault coverage. Born in the test community, design fault coverage finds mutations such as accidental gate substitutions in gate-level net-lists and addresses the observability of faults.

"If you have a mistake in your circuit and your code-coverage method exercises the place where the bug is, but the bug doesn't become visible, at an insertion or the output of the circuit you are not going to notice it," Dill said. "It is going to give you a false sense of security. With this test methodology they solve the problem because they are worried about the observability of faults."

Tag coverage is another semi-formal solution recommended by Dill. It is like design fault coverage, but works at the HDL level.

Dill said one of the most valuable semi-formal technologies is multiple-finite state-machine coverage.

Multiple FSM makes sure that "every state has been visited by your tests, or you can look at transitions between the states," said Dill. "Those transitions can be paired with old states and new states."

Dill also endorsed technology that automatically generates tests for simulation from coverage measurements. He helped develop a multiple FSM and on-the-fly test generator tool called 0-in Search.

Still another semi-formal verification technology is symbolic simulation. "The philosophy of symbolic simulation is to get a lot of coverage from a few simulations," said Dill. "Instead of making the best use of our simulator, we want to have a new simulator that can do a really wide test so that you can do a small number of simulations and cover a lot of cases."

Although symbolic simulation has been used as a formal verification technology, Dill said he promotes it as a technology that can be used between simulation and formal verification as a partial-coverage symbolic simulation.

In addition to these semi-formal verification technologies, Dill promoted forward model checking and prioritized model checking.