Some of the most significant new logic-verification technology seen in years will take center stage at next week's Design Automation Conference in San Francisco. Developments such as a "second-generation" formal-verification tool from Cadence Design Systems Inc., reconfigurable-computing-based products from Axis Systems Inc. and Quickturn Design Systems Inc., and synthesized logic checkers from 0-In Design Automation Inc. may dramatically reshape the chip-design environment.

These offerings arrive at a time when new ideas are desperately needed, given that verification has become a huge bottleneck for large chip designs. In many companies, verification efforts consume most of the design resources, and there are more verification engineers than designers.

"It seems like there is no way, without being able to fundamentally change the approach, to get greater-complexity designs out the door in less time with fewer people," said James Herndon, staff design engineer at Tandem Computers (Cupertino, Calif.). Herndon said verification consumes a "significant majority" of the design cycle at his company.

At Hewlett-Packard/Convex (Austin, Texas), verification probably consumes 95 percent of the CPU cycles and takes around two-thirds of the chip-design effort, said Jeff Quigley, CAD tools group manager. "The biggest problem is knowing when we're done," he said.

Kurt Baty, consultant at Argon Networks (Littleton, Mass.), is running into many verification problems with a chip design that may reach 5 million gates. "The problem is not synthesis or verifying code, it's getting the bugs out of it," he said. Baty noted that "bug density" is holding steady at around one bug per 100 lines of HDL code, even if a design has 200,000 lines of code.

"We need a tremendous amount of help verifying these large ASICs," Baty said. "Anything that even holds a promise of helping us out is going to be very exciting."

Many EDA vendors coming to DAC hope to offer more than a promise. EDA market leader Cadence Design Systems (San Jose, Calif.) this week is making its first commercial foray into formal verification with Affirma, an equivalence checker that claims an ability to handle large designs with easy debugging.

Startup Axis Systems (Sunnyvale, Calif.) will give private demonstrations of its ReConfigurable Computing (RCC) engine, which promises a relatively low-cost way to speed register-transfer level (RTL) simulation by orders of magnitude. Emulation market leader Quickturn Design Systems (Mountain View, Calif.) is also expected to announce reconfigurable-computing technology.

0-In Design Automation (San Jose) last week introduced what it calls the EDA industry's first "white box" verification tool. That company's 0-In Check automatically synthesizes checkers that run with simulation tools.

Other new logic-verification technology includes hardware/software coverification and dynamic code coverage from Systems Science and formal-equivalency checking from startup Verplex. Existing simulation and verification tools are being enhanced with new libraries, features and capabilities.

Formal-equivalency checking is not a new idea; it's been used successfully for several years to verify that functionality is unaffected as designs move from the register-transfer level through various gate-level iterations. But Cadence believes it has enough new technology to compete successfully with market leader Chrysalis Symbolic Design, as well as Synopsys Inc., which introduced its Formality equivalency checker earlier this year.

Based on technology developed at Cadence Berkeley Labs, Affirma promises to quickly verify multimillion-gate designs and pinpoint problems with Cadence's existing SimVision debugging environment. Innovations claimed by Cadence include a new way of combining multiple algorithms, an integration with event- and cycle-based simulation, and an ability to compare RTL code to post-layout physical net-lists.

Cadence is also offering a free formal model-checking tool at its Web site. The tool was developed by Ken McMillan of Cadence Berkeley Labs and is based on the Symbolic Model Verification language.

Formal equivalency checking is still a difficult technology, said Patrick Scaglia, vice president for research at Cadence Berkeley Labs. He said Affirma can help solve "real problems" by verifying designs that diverge widely between the original specification and a downstream implementation, processing deep combinatorial logic and mapping sequential elements without user intervention.

The checker is built around Cadence's Interleaved Native Compiled Architecture (Inca) simulation environment, and is tightly linked with the recently announced Affirma cycle-based and event-driven simulation tools. The equivalency checker shares a common user interface with these tools and uses the same SimVision debugging environment, which provides RTL source highlighting, a simulation waveform display and a schematic viewer.

At the core of Affirma, said Vigyan Singhal, research scientist at Cadence Berkeley Labs, are multiple algorithms that are tightly linked. Other vendors have multiple algorithms, but Singhal said Cadence's approach provides more concurrency. Affirma breaks designs into smaller pieces, called "cutpoints," by identifying internal net pairs that are functionally equivalent. It then takes each cutpoint pair and applies multiple algorithms that operate at a very fine level of granularity.

Algorithms that might be employed include binary decision diagrams, satisfiability, structural matching and random simulation. Intermediate results from each algorithm can be shared by the next.

Affirma lets users go all the way to silicon by checking RTL code against physical net-list files in Cadence's DEF format. Users can thus check for unwanted functionality changes due to place and route, clock-tree insertion or in-place optimization.

"I would never say we can handle any arbitrary design," said Singhal. "If you try to compare 64-bit multipliers with different architectures, yes it will have problems, but so will everybody else's tool. But with multipliers with similar architectures, it should shine."

Affirma got a road test at Audio Digital Imaging Inc. (Arlington Heights, Ill.), where it was used to verify a 1.1-million-gate MPEG decoder chip. "The time to complete gate-level simulation is out in infinity, since we're dealing with huge blocks," said Jean Monroe, chief executive officer at Audio Digital Imaging. "When we can use a tool to evaluate gate-level accuracy within a two-hour period of time, and tell us the gate level is in accordance with RTL, that gives us a pretty high degree of confidence."

The Affirma tool was actually run by Cadence design-services engineers, who made up the majority of the chip-design team. Ted Scarzamalia, manager of Cadence's Austin design center, said Affirma was able to verify 250,000-gate blocks in less than two hours.

Scarzamalia said formal verification was especially important for the MPEG chip, which required designers to run some 94 compliance streams representing up to 20 minutes of real-time operation. "The shortest acceptance stream we had was four seconds of video and audio, which at the RTL takes three days [to run]," he said. "Take it to the gate level and it's impossible."

Scarzamalia said his team ran a minimal amount of gate-level simulation to check out clocks and resets, but otherwise relied on Affirma. They also used the product to check RTL code against the post-layout net-list, and that constituted the chip's final sign-off.

Cadence isn't the only company promising new technology in equivalency checking at DAC. Startup Verplex Systems Inc. (Santa Clara, Calif.) will preview its Logic Equivalence Checker, which like Affirma promises fast performance with user-friendly debugging. Verplex also claims advanced sequential-mapping techniques that require little user intervention.

A new version of an existing product, StructureProver from Verysys Design Automation (Fremont, Calif.), also promises improved debugging and an ability to handle multimillion-gate designs. To be announced this week, StructureProver II includes a graphical user interface with built-in diagnostics that help users locate errors.

The debugging environment provides HDL, schematic and results "views" of the design, cross-annotated between the different windows. Designers can switch between views to control the verification task. Schematic diagrams are annotated with values that can help users see which components led to two non-equivalent functions in the design under comparison.

There's a reason why Cadence, Verplex, Verysys and others are all trying to simplify the debugging problem. It's because equivalency checkers have acquired a reputation for results that are difficult to interpret.

David Baker, vice president of the Austin-based media-accelerator startup Equator, has many good things to say about the Design Verifyer product from Chrysalis Symbolic Design (North Billerica, Mass.). He uses it "every which way" to compare circuits from RTL to post-route net-lists. But, he said, "it is extremely painful to figure out what it's telling you. It tells you what's wrong, but interpreting the results is more an art than a science."

HP/Convex is using an internal tool for formal model-checking, said Quigley. He said it offers very fast performance, because it's limited to a set of standard Verilog constructs the company supports. But his company is evaluating commercial tools in hopes of finding one with equivalent performance and a good debugging environment. Quigley commented that the technology behind Cadence's Affirma "looks solid," but didn't say if HP/Convex plans to adopt it.

Formal equivalency-checking can verify that one design implementation is identical to another, but it can't tell whether functionality is correct to begin with. That task falls to simulation, which is painfully slow for complex chips. Axis Systems is coming to DAC with a new way to speed simulation that is based in reconfigurable computing.

Axis' RCC engine will probably be classified as part of the emulation market, but it's very different from conventional, standalone emulation systems. Physically, it consists of a set of FPGA-based boards inside a Sun workstation. While not as fast as gate-level emulation, the tool maps RTL designs into customized processing elements, and offers debugging under software control at the RTL source level.

J.H. Chang, vice president of engineering at Trident Microsystems (Mountain View), is a beta site user of Axis' RCC as well as a customer of Quickturn Systems' Realizer emulator. To avoid purchasing hardware that may become outdated, he uses Quickturn's design services and lets Quickturn do the mapping.

Compared with all other verification methods other than emulation, Chang said, Axis' approach appears to be fastest. "They are claiming about 100,000 cycles per second, which is probably 100 to 1,000 times faster than using C modeling," he said. "That is something like 5,000 to 50,000 times faster than Verilog."

While emulation systems can be difficult to use, Chang said, the Axis RCC offers a user interface that is more "software-based." Because it works with RTL code, he noted, users can start to work with the RCC much earlier in the design cycle, long before a design is "stable" enough to be mapped into a gate-level emulator.

"Both have their strengths," Chang concluded. "Axis' strength is from the beginning to the point where you stabilize your design. The majority of the design time is spent in this phase, so the Axis RCC tool can significantly cut overall design time. Emulation has a higher initial investment, but once you reach a certain point you can run a lot more applications."

Capacity to rise
Chang said he hopes Axis will soon increase its capacity limit. Axis is currently quoting a million-gate capacity, but plans to raise this in the future.

One strength Axis claims is easy setup and use, which is not the case for big emulation systems.

Equator's Baker is a satisfied user of Quickturn's Cobalt emulation system, but he acknowledged that setting it up is "probably one of the hardest things I've done in my life." Tandem's Herndon, a longtime Quickturn user, said that there's a "significant hardware burden" involved in setting up the system.

For its part, Quickturn is also expected to announce reconfigurable-computing technology at DAC. The company isn't yet revealing product details, but Naaem Zafar, vice president of marketing, shared some of the company's perspectives.

"If you can take an algorithm and compile it into reconfigurable computing, which is now dedicated to run the algorithm in an optimal way, you get a tremendous performance boost," he said.

Zafar said there are plenty of "hard-to-compute" problems in EDA that could benefit from reconfigurable computing. In addition to event-driven simulation, he said that electrical-rule checking, design-rule checking and placement and routing are all good candidates.

But there will still be a need for traditional emulation, Zafar said, because it lets users go "in circuit" by plugging into the target system. "Traditional emulation will always have a place for system development," he said. "Some of the regression engines may be replaced with reconfigurable-computing assisted verification."

Narrowing the scope
While reconfigurable computing can dramatically speed simulation, 0-In Design Automation is offering a way to make simulation much more effective. Its 0-In Check product, now in use by several development partners, synthesizes checkers that literally "zero in" on specific types of problems while simulation is running.

The net result, according to the company, is a set of checkers that can directly find bugs that otherwise require unrealistic amounts of simulation. Checkers look for such problems as register leaks, counter overflow and underflow, simulation-to-circuit mismatches and function variables that retain previous values.

0-In presents the product as the first white-box verification tool, meaning that it looks at a design's internal structure rather than its outputs. 0-In Check synthesizes checkers from RTL Verilog net-lists. An upcoming white-box tool, 0-In Search, will provide further analysis of difficult "corner-case" bugs.

Baty at Argon Networks is using 0-In Check to help verify Argon's Internet switch and router chip, which is approaching 5 million gates. "In a nutshell, it uses a synthesis methodology to generate assertions about your design," he said. "The problem with formal verification tools is that they don't make any statements about what your design should be doing. 0-In studies your code and tells you what it should be doing."

In essence, Baty said, the tool incorporates rules about good design practices and makes sure the design observes them. "The checkers aren't doing anything the simulation is not doing already," he said, "but what they're doing is giving you visibility into problems you might not notice."