Design Automation

Readers Speak Out on DSM: Part 2

Our three-part report on readers' experiences with deep-submicron design continues. This installment focuses on design verification in general and offers strong opinions on formal verification in particular.

by Jonah McLeod

Last month, we reported on some of the results of a survey we conducted in July to determine our readers' experiences designing circuits implemented with deep-submicron (DSM) processes. The questionnaire examined how the readers are designing DSM circuits and what new methods they are employing to cope with the special problems such design poses. This month we present more results.

The first half of the survey, reported on in November (p. 16), dealt with the design flow. Here, we consider the problem of design verification, and next month we'll report on the final part of the survey, dealing with signal analysis and the use of ASIC vendors' proprietary tools.

To test the premise that complex ICs require more verification, we asked how much of the design cycle readers devote to verification and what verification tools help them perform the job.

Industry analysts claim that 60 percent of the design cycle is spent performing verification. We asked our readers: "Is 60 percent an accurate figure? If not, what is a more realistic amount?"

"Indeed, 50 to 60 percent is a realistic figure, and I expect it to remain so given the growing complexities of designs," says Yaron Wolfsthal, formal verification manager at IBM Corp.'s Haifa Research Laboratory in Haifa, Israel.

"The 60 percent estimate is accurate for ICs of around 150,000 gates," says P.G., a designer wishing to remain anonymous. (Initials are used throughout for respondents who asked not to be identified.) "The percentage of time spent verifying the design has increased not just because of complexity, but because the designing part is taking less time, even for a more complex IC. Just look at how quickly you can write a few hundred lines of Verilog and synthesize 10,000 gates. Thus the design of more complex ICs has shortened, but the verification phase has lengthened."

Trocine Thomas, senior engineer at Distributed Processing Technology Inc. in Maitland, Fla., puts the figure higher: "Design verification is the area of ASIC design on which the most time is spent, regardless if it's 3.0 µm or 0.18 µm. I would estimate that more than 80 percent of the designer's time is spent verifying design functionality and timing during all phases of the design."

Another reader also puts the figure higher than 60 percent, based on a broader definition of verification. "Functional and timing verification are ongoing through most of the process," asserts Sean Curry of IBM Corp.'s Global Procurement, Logic Technology and Qualification in Austin, Texas. "Once a part has been manufactured, it's verified at the factory, and then verification is performed in the lab environment. If added in, these activities are a significant portion of the total design cycle."

"Verification lasts for the duration of the project," K.C. agrees. He adds that it "can be the critical path of the project if not properly staffed and supported."

For B.H.'s company, verification is indeed the critical path. "On most designs," he says, "we now create a separate simulation team in charge of verification to try to parallel the work and speed up the design cycle. That works well except that most guys don't want to be on the sim team, as they would prefer to be doing the logic design instead."

Yaron Wolfsthal of IBM says up to 60 percent of the design cycle is tied up in verification.

Although not giving any figures, K.C. makes what could serve as a final comment on the subject: "ASICs with a million gates require time and effort to verify. Environments and tool suites need to be set up and maintained, and those efforts may constitute a project of their own." The efficacy of equivalence checking With the increase in time spent on verification, we wanted to determine what new tools designers are using. We asked: "Suppliers of design verification tools claim that there are two parts to the problem. One is ensuring that the design, once defined, does not deviate from the golden specification. These equivalence-checking tools, such as Chrysalis's Design Verifyer, ensure that once an HDL specification is completed, subsequent changes in gate-level implementations are equivalent to the original specification. Have you had any experience with such tools, and did they shorten the design cycle significantly?"

(Note that because equivalence checkers were the first formal verification tools to appear commercially, and because we specifically called them out in our question, many respondents use the terms "formal verification," which encompasses a variety of techniques and approaches, and "equivalence checking" interchangeably.)

The responses were decidedly mixed. Several respondents are extremely negative about equivalence checking, whereas others are strong supporters. Some see its potential usefulness but believe that the tools available need to mature a bit more.

"Formal verification tools and the entire concept of formal verification look like a solution in search of a problem," B.H. says. "We used this flow on one design and the guys doing formal verification never found a single bug. We would have been better off using them to do simulations."

He continues: "I think there's a role for formal verification in the design flow, but I sense that the proponents of it are overselling what it will do in an attempt to create a market for it. I haven't met a single hands-on designer who felt that formal verification was crucial to the design, though several managers were enamored with it."

Designers performing completely automatic design flows also find equivalence checking of little value. "We try to keep our implementation flow 100 percent automated," says Doug Warmke, hardware director at Ikos Systems Inc. in Cupertino, Calif. "There's virtually no hand tweaking allowed, since we can't afford the time wasted by nonrepeatable processes. Equivalence checking doesn't fit in well with this philosophy, because all database iterations are supposed to be correct by construction."

Adding support for Warmke's assertion, Matt Hsu, manager of ASIC design at Shomiti Systems Inc. in San Jose, explains why he sees no real need for equivalence checking. "If you don't trust your synthesis tool to create functionally correct netlists, you should throw it away. Further, synthesis is fast enough that there shouldn't be a reason to play around with the gates, invalidating the whole directory of regression tests that were developed for the RTL code. Of gate-level problems, 99 percent of those I've seen are related to library or timing issues. Our 'golden specification' is on paper. How does the equivalence tool check against that?" (See also "All That Glitters. . . . ")

"If you haven't taped out yet, why not just resynthesize?" Hsu asks. Then he adds, "For designs that have already taped out, I've run subsets of the RTL simulations successfully on a modified gate-level netlist to verify function and static timing analysis to verify timing."

Nancy Nettleton, ASIC design methodology manager at Sun Microsystems Inc. in Mountain View, Calif., agrees with Hsu's basic assertion. "This sort of verification is only important if you don't trust your mapping from RTL to gates."

The inability to verify multipliers is a shortcoming that Russell Ray, a staff engineer at Mitsubishi Semiconductor America, Inc. in Durham, N.C., cites as a reason for not using equivalence checking. "We've evaluated these tools but haven't added them to our flows yet. We found that they lacked the capability to verify large parts of designs containing multipliers. Because of the large number of multipliers we use, we encountered a major problem partitioning the design so that the tool could verify everything else. We finally left it with a promise from the vendor to get better support for multipliers and haven't looked at them since."

C.M. gives a different reason for his lack of interest in equivalence checking: "The equivalence checker is employed when functional verification is completed through functional testing. This process accounts for 90 percent of the verification cycle, after which the RTL, the golden specification, stays frozen. That being the case, the usefulness of equivalence checkers is exaggerated. Because they account for time savings in about two regression runs, the time and effort spent getting the tool working may not be worth the savings."

All that glitters . . .

Sandro Pintz of VM-Labs says the golden specification changes over time.

Besides the general comments about equivalence checking, some respondents are critical of the idea of a golden specification. "The 'golden specification,' what a laugh!" proclaims B.H, who speaks from 16 years' experience as a designer and design manager building custom microprocessors, as well as standard-product ICs and ASICs. "Every project I've ever worked on had to contend with spec changes up to the last moment. It's the nature of our business." Sandro Pintz, senior design engineer at VM-Labs in Los Altos, Calif., also has a problem with the concept. "Is it today's 'golden specification'? Tomorrow's? Is it the one that will fit in the die and meet timing, or the one that marketing wants?" he asks. "Specs change way too often. Some tools that provide specific constructs to enhance your ability to produce testbenches quickly and effectively could be of great help, such as Systems Science's Vera verification language, which I've used in a few designs." "Because of the nature of the market, it's very rare that a design, once defined, doesn't deviate from the golden specification," says Thomas Dejanovic, ASIC design engineer at Cisco Systems Inc. in San Jose. "In fact, in my seven-year career in ASIC design, that has never happened."

Although he is more positive, David Lau, a senior staff engineer at QED Inc. in Santa Clara, Calif., also questions the usefulness of equivalence checking: "Though equivalence checking is a good tool and does its job--checking between schematics and HDL--the real problem is how to check that the HDL is correct," he says. "Equivalence checking is only two percent of the whole problem. Even other formal methods, like theorem proving, can only solve small chunks of a very large problem."

Cesar Maldonado, a design engineer for Philips Semiconductors in Albuquerque, N.M., gives another view. An equivalence checker, he says, "is just an intermediate tool, useful in making sure we don't deviate from the original RTL because of synthesis, testability, and manual modifications. That's good but not sufficient for the goal of ensuring that the design meets its specifications."

Believers Despite the negative views of some, many are indeed strong supporters of equivalence checking.

"Designing and verifying a design at the RT level is the most productive path to a functionally correct design," notes D.L. "Once that's done, it makes no sense to continue simulating the function after synthesis to gates, again after adding test logic and clocking structures, and once again after layout."

For D.L., the key to eliminating the extra simulation runs is an equivalence checker. "These design transformations are not intended to change the design's original function," he explains. "Tools that do Boolean equivalence checking after each of those transformations have replaced days to weeks of gate-level simulation, which provides only partial coverage, with a run taking less than a day and that proves that all functional paths remain unaffected. With chip designs of well over 100,000 gates, it's hard to see how one can be successful without Boolean equivalence checking."

IBM's Wolfsthal agrees. "Boolean equivalence checkers are indeed a useful and essential part of a modern-day verification methodology," he says.

Howard A. Landman, a staff design engineer at Toshiba America Electronic Components Inc. in San Jose, enumerates the main advantages of equivalence checking: "Sometimes you can get 100 percent confidence, which is usually impossible for simulation, and because it's easier to work at any level of the hierarchy--simulation vectors are usually written at the chip top-level only--often it can be faster and require less memory."

Says R.M., "We've used equivalence-checking tools on designs for which we have two representations of the design, i.e., schematics and layout or gates. The two representations are created by different people using different tools, so this is the kind of problem those tools were made for."

Yuqian Cedric Wong of Motorola cites formal methods as an effective alternative to vigorous simulation to achieve 100 percent assurance of design verification.

Yuqian Cedric Wong, lead engineer at the Motorola Inc. Cellular Infrastructure Group's Advanced Cellular Products Division in Arlington Heights, Ill., adds support as well: "We're using a formal verification tool to verify insertion of scan and BIST, plus clock and reset. We're also using these tools to verify scan reordering and ECOs." Wong believes that design time could be reduced by a thousand times or more. Furthermore, he notes that equivalence checking provides an accuracy of 100 percent, whereas simulation provides an accuracy of somewhere between 60 and 90 percent, depending on the complexity of the design. P.G. agrees, stating that complexity demands formal verification. "As designs get exceedingly large, it becomes exponentially more difficult to exhaustively verify them," he claims. "I believe formal verification will have to become part of the process." The operative phrase here is "will become." Many respondents believe that formal verification tools are not yet ready for prime time.

Although Mitsubishi Semiconductor decided not to use an equivalence checker, "That doesn't mean we won't use these tools," Ray says. "We feel that we'll have to use them in the near future--within the next year--and that the tools were in their infancy when we evaluated them."

Verifying Design Verifyer

Shuhui Lin, at Alcatel Network Systems, found an unexpected, undriven output in a postscan netlist with DV and the experience sold her on the usefulness of formal verification tools. One of the deficiencies in the questionnaire was the inclusion of a specific product, Design Verifyer (DV) from Chrysalis Symbolic Design Inc. of North Billerica, Mass., in the question on formal verification. As a result, many readers commented extensively, both positively and negatively, on the tool. "We ran Design Verifyer in parallel with regression simulations to give us an extra measure of confidence across revisions of our design," explains Shuhui Lin, technical staff engineer at Alcatel Network Systems Inc. in Raleigh, N.C. "In one instance, DV reported an unexpected, undriven output in the postscan netlist. Although this pin wasn't needed for functional purposes, it was needed for testability. Detecting this type of problem before layout is one example of how DV or other equivalence checkers can be extremely useful." Howard A. Landman, a staff design engineer at Toshiba America Electronic Components Inc. in San Jose, cites the example of a timing fix made to one small module of a large chip. "Using DV, we verified formally that the function of the module didn't change. We only needed to examine the new and old versions of that one module to prove that. Using simulation, we would need to build a model of the entire chip and simulate it--usually with a small subset of our total set of vectors. In this case, DV can provide 100 percent confidence in a short time, and simulation can provide only partial confidence and may take longer because it's working on vastly larger data." Anders Nordstrom, a senior ASIC designer at Northern Telecom Ltd. in Ottawa, puts some numbers to the time savings: "In one case, RTL simulations took 30 minutes, and gate-level simulations, with no timing, took four hours. It still takes time to run formal verification and static timing analysis, but both are limited tasks. After one run of each tool, you know if you pass timing or if two circuits are equivalent." Brian Snider, senior design engineer for Centaur Technology Inc. in Austin, reports an even greater time savings: "I'd say that routine equivalence checking saves several days' time per design cycle." His company uses Design Verifyer to perform equivalence checking on both synthesized and full-custom portions of their chips. "It also gives you a better sense of confidence in the final design and allows last-minute fixes for timing and functionality without losing days in reverification with cycle simulation," he says. On the downside, Jon Stahl, senior designer at Avici Systems Inc. in Chelmsford, Mass., describes the drawbacks he encountered with Design Verifyer. "In my experience, Design Verifyer is an excellent tool. However, the learning curve prevented us from seeing a schedule speed-up. We expect to see about a 20 percent cut in time and man-hours." His observation is echoed by Rob Maffit, chief technical officer at Prescience in San Carlos, Calif. "The start-up time to get a project set up with Design Verifyer is too long, but it's a necessary evil." Lin says that Alcatel continues to see benefits in using Design Verifyer as the company develops more expertise with the tool, but they've found a limitation. "So far we've had the most success with a bottom-up approach in verifying a hierarchical design. We've also found that it's much easier to compare netlists that have gone through one transformation than netlists that have gone through several transformations. For example, it's easier to compare an RTL netlist with the synthesized gate netlist than it is to compare the same RTL with a postscan netlist containing JTAG scan and clock tree synthesis. Therefore, to reap the benefits, it appears best to adhere to a methodology in which the equivalence checker is used at every stage of the netlist transformation." K.P. complains that the tool does nothing to reduce design time. "The designs we do are very custom and don't focus on reuse. Therefore generating new vectors is always required. Without having the golden design sitting in the wings waiting to be checked, we're required to proceed through simulation to obtain the full functional verification." "We've also experienced issues in which the original netlist submitted to the vendor couldn't be compared with the final postprocessed netlist," he adds, "but only with a netlist two or three steps before the final one. Although this limitation could be viewed as beneficial, Design Verifyer does not offer the complete solution that I've heard people boast of." Another designer complained about the tool's inability to handle large multipliers. "That meant we would have large areas of our design that couldn't be verified," says D.L. "We opted to stay traditional." But he adds, "I still see lots of potential in this technology. We often inherit RTL and gate-level VHDL, and one wonders if they describe the same design." Anders Nordstrom of Nortel says formal methods achieve in minutes what simulation takes hours to do.

"We evaluated formal verification tools extensively, and at the time we found them to be a little immature," agrees Kip Lebar, manager for ATM switching ASIC development at Cabletron Systems Inc. in Rochester, N.H. But he continues, "I believe that formal verification will be ingrained in the development flow in the next 6 to 12 months."

One of those who plans to adopt equivalence checking soon is M.S. "We'll be looking into it in the next several months," he says. "We intend to use it mainly for checking gate-level netlists against each other during our timing ECO process, although we will do RTL to gate-level checks, especially when Synopsys sends out a warning about generating bad logic. Some of the issues that we'll be looking at will be the handling of pre- and post-scan netlists, how the tool handles various pipeline balancing operations-- Synopsys behavioral retiming, pipelined multipliers, and so forth."

Cesar Maldonado, a design engineer for Philips Semiconductors in Albuquerque, N.M., gives another view. "An equivalence checker is just an intermediate tool, useful in making sure we don't deviate from the original RTL because of synthesis, testability, and manual modifications. That's good but not sufficient for the goal of ensuring that the design meets its specifications."

At least for some cases Even some of those who are generally negative about equivalence checking support its use in special cases. Sun's Nettleton, for example, describes two instances to which equivalence checking might be applied: hand mapping of RTL to datapath structures and the use of home-brewed in-place optimization scripts to do buffer sizing for final performance improvement. But she contends that "those are pretty isolated occurrences, limiting the use of formal verification technology."

Others are more positive. Says Shomiti Systems' Hsu, who, like Nettleton, believes in the reliability and efficacy of synthesis, "There are reasons to do gate-level hacks, but they must be done very carefully and very minimally. Equivalence tools will be useful here if you want to change the VHDL to reflect the same function."

Equivalence checking could help when using beta versions of new tools, Ikos's Warmke says. "If we had requirements that demanded a tool with special features, but the tool was immature and didn't always provide correct-by-construction results, then equivalence checking would be indispensable."

Formal verification, though, doesn't end with equivalence checking. It includes symbolic model checking, which checks a design for conformance to a functional model and is now available commercially as well.

"Simulation against the golden specification is the much simpler component of verification," says Peter Feeley, project manager at Advanced Hardware Architectures Inc. in Pullman, Wash.

Checking at the top "To meet the challenges inherent in the ever increasing complexity of micro-architectures, advanced verification technologies are required, such as high-level modeling languages and powerful formal verification tools--for example, symbolic model checkers," Wolfsthal of the IBM Haifa Research Laboratory says.

IBM presented RuleBase, a symbolic model checker, at this year's Design Automation Conference. The tool has been used advantageously across IBM's hardware divisions, Wolfsthal reports, and the company is expanding its use.

"I would be much more interested in 'easy-to-use' model checking than in equivalence checking," Warmke says. "That could possibly save a lot of time chasing down corner cases in verification and make some designs possible that previously were unthinkable." *

To voice an opinion on this or any Integrated System Design article, please e-mail your message to miker@isdmag.com.

integrated system design  December 1997