Unisys & Synopsys Synopsys' Formality Tool Helps Unisys Project Slash ASIC Redesign Time

In order to improve the performance of the ClearPath(TM) HMP NX servers, Unisys engineers decided to redesign the processor into a CMOS process, and to add additional performance through architectural changes. Formality®, Synopsys' formal verification tool, allowed the team to verify their design in minutes instead of weeks usually required with gate level simulation.

Formality Benefits

• Easily adopted into existing design flow
• Shortened verification time from 17 days to four
• Enabled engineers to identify and fix bugs that were impractical to find with gate-level simulation

In the high stakes world of mainframe computers, performance and reliability are everything. Unisys is a leader in this highly competitive market, providing computer systems to customers with mission-critical, round-the-clock applications such as banks, airlines, hospitals and insurance companies. In order to maintain and grow market share, Unisys must continue to increase the capacity of its systems and simultaneously improve product quality.

The ClearPath HMP NX family of enterprise servers is one such key product line in the broad Unisys product offering. Unisys ClearPath enterprise servers feature the industry-leading Unisys Heterogeneous Multiprocessing (HMP) architecture, which enables customers to run legacy mainframe applications and databases and those based on UnixWare and Windows NT side-by-side in the same server.

In order to increase the market share of ClearPath HMP NX servers, a succession of performance improvement projects were planned, each addressing independent system bottlenecks. By redesigning a few ASICs at a time, Unisys could better manage its investment and rapidly deliver product improvements to customers.

The work of redesigning these large NX series transaction processors first began in early 1995. Architectural changes, ASIC design work, design methodology and simulations were all done locally by small sub-system design teams. Mark Jennion, a group manager in one of these hardware sub-system groups, directed board test, ASIC test and design verification methodology for this effort. "To this point, our machines were mostly ECL. The first objective here was to redesign the main processor into all CMOS and to add additional performance through architectural changes," said Jennion. "This had to be done gradually, a sub-system at a time, because it's too risky to redesign the whole system at once."

At the heart of the ClearPath HMP NX server architecture is a processor complex that supports the Unisys Master Control Program (MCP) environment, as well as the open Microsoft Windows NT environment. The ClearPath HMP NX4820 Series Processor Module (PM) contains an Instruction Processor (IP), Second Level Cache (SLC) control and 1.5 MB of SLC RAM storage. The IP is the basic processing element within the PM and is a single-chip design fabricated in 0.5-micron CMOS technology.

The first project to be completed was a redesign of the IP and SLC, targeting CMOS technology for performance and fabrication cost benefits. These chips are at the very heart of the processing system and the changes promised to provide significant overall system improvements once deployed.

"Formality has prevented three bugs, and we've only been using it for about nine months. It will be an integral part of all of our future NX series ASIC design efforts."

Mark Jennion,
Group Manager, Hardware Sub-System Group

Time-to-Market Pressures

Exhaustive simulation of the gate-level design was out of the question, because of the complexity of the targeted ASICs. "The single chip instruction processor has several large internal RAM structures and about 395,000 gates of complex logic and the second level cache ASIC has internal RAM and about 275,000 gates," Jennion points out. "This meant that comprehensive, iterative gate level simulation wasn't feasible." A different approach was needed in order to prevent problems from effecting progress of the redesign program.

"Each of our CMOS ASIC designs experienced a number of functional engineering change orders (ECOs), each one requiring full-chip verification," Jennion says. "We had to use some sort of methodology that would compare the versions of the design before and after an ECO. We developed a homegrown verification method to ensure that each change didn't inadvertently affect working logic. We used the vectors from the original working design and compared those to the simulation file after the ECOs were implemented. Then we could see if any changes were due to the intended ECOs or because of an inadvertent change. That method worked well for finding problems, but was time consuming."

On average, the vector generation took from five to 12 days, followed by one to two days of simulation. An engineer then spent one to three days sorting out the results. Clearly, a less time consuming method had to be found. After using the homegrown method for nearly two years, Jennion began to investigate the formal verification equivalence checking tools that were being introduced to the market.

Formal Verification Provides a Solution

The formal verification methodology Jennion was considering would allow his team to compare the functional equivalence between two versions of a design in a matter of minutes or hours, instead of the weeks required by a gate-level simulator. However, to be truly effective as a replacement for exhaustive gate-level simulation, Jennion knew that a formal verification tool must offer more than capacity and speed. It must also provide fast and easy debugging of design errors, be usable in a broad array of design types and applications, and be easy to integrate into existing design flows.

The Formality Product Provides Needed Verification Strength

Jennion's team also used the Formality tool to compare versions of the design throughout its development cycle. In a typical flow, they found that the Formality tool could reliably compare the functional equivalence of the RTL source to the post-synthesis, gate-level netlist. The Formality solution could then be used after each ensuing step to maintain complete functional equivalence at the gate level during subsequent stages of the flow.

Jennion's team compared VHDL to EDIF, EDIF to EDIF and VHDL to VHDL. Much of their use of the Formality tool was running comparisons on sub-blocks of the entire device. However, the real value was realized while verifying complete designs. "Saving from one to two weeks for each ECO not only preserves valuable time to market," says Jennion, "it's a great reassurance that working logic hasn't been broken by an ECO."

"So far Formality has prevented three bugs, and we've only been using it for about nine months," Jennion points out. "Gate-level simulation never would have enabled us to catch and remove those bugs efficiently. Even our homegrown vector comparison methodology was breaking down."

The immediate result of the project was a successful release of the ClearPath HMP NX5800 and NX5600 server lines in June 1998 and the NX5820 in January 1999. A total of five ASICs were modified in the two released product lines, each one benefiting from the application of the Formality tool for fast functional verification. "We're not only using Formality to redesign current NX series ASICs, we'll be using it as we create upcoming NX product lines. I would consider Formality to be an integral part of all of our future NX series ASIC design efforts," Jennion concluded.