Chris Hoogenboom, manager of ASIC development at Xylan Corporation, was tasked with designing two new ASICs for the company's new Ethernet Switching Modules (ESMs). A leading provider of complete campus switching systems, Xylan looked to these chip sets as a way of leapfrogging the competition in terms of price performance in the company's OmniSwitch any-to-any switch. Xylan is one of the only switching companies to develop its own proprietary ASICs for its switching products.
The Mammoth and Whistler chips are the core of Xylan's ESM-100C-12 and ESM-C-32 Fast Ethernet switching modules.
Using standard chip sets for the switching engine and companion media-access control (MAC) chip would have provided similar functionality, of course, but the off-the-shelf chips would have limited Xylan's ability to drive down overall system pricing. The two proprietary ASICs were key factors in Xylan's ability to achieve its price performance goals. Moreover, as Hoogenboom explained, "The chips would be leveraged into a whole range of Xylan products for some time to come, so the project -- and the chips -- were strategically important to our business."
In addition to the strategic importance of the project, the Xylan team faced a number of challenges specific to ASIC development in the networking industry. Time-to-market was of primary concern. "Given the speed of the evolution of the networking market, we had to get the chips working right, the first time, on schedule, so we could get to market on time," Hoogenboom explained. In addition, as Hoogenboom noted, "Developing ASICs is always a non-standard, non-trivial task." The complexity of the two chips made this project no exception to that general rule, especially for verification. The frame switching engine, called "Mammoth," would turn out to be one of the largest and most complex ASICs ever developed in the networking industry. And the "Whistler" companion chip, an eight-port MAC with autosensing 10/100 megabits per second on each port, represented a significant design challenge on its own. Together, the two chips would handle all the switching and Ethernet MAC-layer protocols for the Xylan ESM products.
Like all ASIC development in the networking industry, Hoogenboom knew designing this chip set would result in a substantial number of changes made by hand to the netlist after the design was in layout. While some hand-engineering change orders (ECOs) are made to fix functional problems found late in the development cycle, the majority made on any project is typically to correct timing. And hand ECOs inevitably introduce bugs into the design. Finding and correcting these bugs represented yet another challenge for the team -- one that Hoogenboom realized would require a formal -- verification tool. "Some of these changes are simply not verifiable by simulation," he explained. "I knew we needed some way other than just good luck and good faith to verify that the changes were, in fact, done correctly."
As the manager of ASIC development, Hoogenboom recognized that his decision on a formal-verification tool would be critical. He had a vested interest in the tool as well, since he was responsible for all the backend work, from RTL through silicon and verification, on the Mammoth ASIC. Four other full-time engineers would perform all the design, simulation, and emulation on the chip, while one full-time designer would handle all coding, simulation, testing, and backend work on the Whistler ASIC.
Deciding to Use a Formal-Verification Tool
Based on his past experience in ASIC design and the project's complexity, Hoogenboom made the decision to use a formal-verification tool early on in the design cycle. A formal-verification tool, he understood, would address the problems ASIC developers typically face in attempting to verify an extremely complex design within the constraints of the market window. ASIC designers in the networking industry are frequently unable to simulate extremely complex designs well enough to validate their functionality. "In the network world, you need an awful lot of vectors to get good coverage of the networking hardware," Hoogenboom commented. "There wasn't enough CPU power in the building to simulate the Mammoth ASIC. Our hand-chosen subset of simulation vectors required eight CPUs running for two weeks, using a lot of market time to achieve partial functional verification. Formal verification is the obvious solution."
Selecting Synopsys' Formality
Using Synopsys' Formality™, Hoogenboom realized, would eliminate whole areas of risk so he and his team could focus on the design challenges of developing such large and complex chips. In the end, Xylan selected Synopsys' Formality for a variety of reasons, not the least of which was Synopsys' expertise in ASIC development tools. "Synopsys has a good reputation," Hoogenboom explained. "The other Synopsys tools we have work very well and are very well supported."
Hoogenboom evaluated two verification tools for two to three months before choosing Formality for its superior performance and capacity. "We tested the tools with a design similar to Whistler, and Formality ran the verification much faster than the other tool," Hoogenboom said. "Plus, Synopsys in general seemed to have a better handle on doing RTL-to-gate comparisons."
Formality's library support and tight integration with Synopsys Design Compiler™ helped facilitate a smooth and relatively uneventful design cycle as well. In addition, the tool fit seamlessly into Xylan's existing development environment, made up of "bread and butter" Synopsys tools, such as Design Compiler, Design Analyzer™, DesignTime™, and Synopsys HDL Compiler™, as well as other third-party tools.
While he ultimately selected Formality based on its own merits, Hoogenboom found his decision was only affirmed by a "close call" Xylan experienced with the Mammoth ASIC. "The bug was fixed rather painlessly," Hoogenboom explained. "But it underscored the fact that mistakes can happen--and that we needed to strengthen our verification strategy." In the end, Formality played a key role in the verification process, proving its value early on in the development cycle.
"Formality saved us months in delay to market as well as substantial sums of money. That alone paid for the purchase of the tool."
Manager of ASIC Development, Xylan Corporation
Using Synopsys' Formality in Xylan's Design Methodology
Formality fit easily into Xylan's existing design flow. After writing the RTL code and generating a netlist for the Mammoth chip, the Xylan team then ran the design through Formality. Within two days of using the tool, Xylan developers found a bug in a hand ECO made to the design, which otherwise would have gone unnoticed until late in the design cycle. "By finding that mistake, Formality saved us months in delay to market as well as substantial sums of money," Hoogenboom said. "That alone paid for the purchase of the tool."
With the Whistler code, the Xylan team simply ran a "top-level verify," reading in the RTL code and gate-level netlist and setting constants to disable scan logic for verification. In the end, the team spent approximately six months each on the coding, verification, and backend stages. During simulation and emulation, the team ran seven simulators and two emulators full time for four months in order to validate the large and complex chips.
Succeeding With Synopsys' Formality
The end result was a chip set that far surpassed anything else in the networking industry. The Mammoth ASIC sets new performance standards, forwarding packets at up to two gigabits per second on the backplane, a speed not possible in previous-generation switches, and supporting various frame protocols for local area networks (LANs) including Ethernet, FDDI, CDDI, and Token Ring. With a higher density than other MAC chips, Whistler provides a higher speed interface than off-the-shelf ASICs, implementing a special H-bus local bus for handling packet transfers from the MAC to the switching engines.
The Mammoth chip is an eighty megahertz, 0.35- micron ASIC, consisting of 500,000 gates, 330,000 bits of SRAM, with seven clock domains, two embedded SPARC processors, frame buffering, frame switching, and a coherent cache system. Overall the ASIC has just under four million transistors. The Whistler ASIC, by comparison a more straightforward chip, consists of 115,000 gates and 50,000 bits of SRAM in a 0.6- micron gate array.
Finding Synopsys' Formality Easy to Use
As an experienced Synopsys user, Hoogenboom found Formality very easy to use. He was able to use the tool after only a few hours of formal training and a tutorial. In addition, Hoogenboom anticipates the tool will be very straightforward even for novice users. On a recent project very similar to Whistler, a Xylan designer with almost no Synopsys experience was able to get up to speed on the tool easily and quickly. "He simply attended the training session, worked through the tutorial, and asked some project-specific questions of Synopsys customer support-and he was up and running," Hoogenboom stated. "It's not a difficult tool to use."
Measuring the Value of a Formal-Verification Tool
Verifying functional equivalence, as Hoogenboom sees it, is the central purpose of formal verification. "The more tests you run, the more likely you are to get better coverage and to find more bugs," he explained. Formal verification, in this sense, is a way of looking at the functionality of a design at a different level. "You're really looking at the equivalence of the design, comparing netlists to RTL," he said. Hoogenboom likens the value of a formal-verification tool such as Formality to a static-timing tool. "You can verify the timing dynamically, but only to the extent that you can sensitize the critical path," he said. "Similarly, you can verify functionality dynamically, but only to the extent that you can sensitize the functionality."
Hoogenboom sees formal verification as soon becoming the norm for verifying functional equivalence. "As you develop larger and larger designs, formal verification becomes increasingly important." He added, "If you want to pull in design schedules, you have to start layout while you're doing functional verifications in emulation and simulation. This process will turn up small bugs that will have to be fixed with hand ECOs." The best way to check these late-in-the-game changes, Hoogenboom believes, is through formal verification.
Looking to the Future With Synopsys' Formality
Although Hoogenboom and his team look forward to the release of the first version of Formality, he doesn't anticipate they will change the way they currently use the tool in the design process. In fact, Xylan has been using Formality fairly aggressively in its pre-announced version, "We have already used Formality on successive projects such as our 'Gore' and 'Mammoth II' designs," Hoogenboom concluded.