Sun Microsystems Uses Mentor Graphics O-In Verification Business Unit Technology on a Three-Million Gate Design
Sun Microsystems, a world leader in enterprise computing solutions, manufactures workstations and high-end servers that maintain some of the highest sustained bandwidths and some of the lowest latencies of all servers in their class. Paul Gingras, design verification manager at Sun Microsystems, was responsible for the verification of a large ASIC developed for a high-end server with several very large, very complex components.
“My objective is to get into as many corners of the design as I can. Questa Search helped us explore those aspects of the design.”
Learn More About O-In Verification Business Unit Technology
product overview: The Questa Formal Verification tool complements simulation-based RTL design verification by analyzing all possible behaviors of the design to detect any reachable error states.
Major product features:
- CheckerWare® checkers improve observability of difficult-to verify logic
- Questa® Search amplifies testbenches to exercise corner cases missed by directed and pseudo-random testbenches
- Questa Search finds bugs early in the design cycle, improving time to market
- Questa tool suite provides a high level of confidence that the design is ready for tape-out
Assertion-Based Verification Exercises Corner Cases in High-End Server ASIC Design
Late in the design cycle for this ASIC, a complex delay-limiter module was added to control transactions that flowed through the device. The new logic interconnected many other modules in the design and employed a complicated arbitration scheme. At this point, the design reached a daunting three million gate equivalents with over 800 I/O pins. Sun determined that writing directed tests to analyze all potential corner-case behaviors would be very difficult and time-consuming.
“One of the major challenges we faced was how to improve upon the random aspects of conventional simulation,” said Mr. Gingras. “We needed to improve the coverage on the design before tape-out.” Sun turned to Questa’s Assertion-Based Verification (ABV) Suite for help with the verification hot spots in this design, including the new delay-limiter module.
Questa Check Enables Valuable Assertion Methodology
The development team at Sun employed sophisticated design and verification methodologies that combined RTL simulators with commercial testbench and coverage tools. Questa’s ABV Suite added critical capabilities not found in these tools. By analyzing the internal structures of the ASIC design, ABV technology attacked the two primary functional verification problems: limited observability and insufficient controllability.
The Questa tools enhanced observability within the ASIC design by using the CheckerWare library of checkers. Checkers are assertions that are supplemented with statistics gathering and corner- case-analysis logic. Checkers help developers document, validate design interfaces, and grade test suites using the industry’s most rigorous metrics. Since checkers are written in RTL, they are independent of the particular testbench and verification language used.
Using Questa’s rich CheckerWare library, the ASIC designers captured their assumptions and obtained maximum design checking with minimal specification. “Questa fit in really nicely largely because it followed our existing methodology in terms of inserting statements in the design or assertions for capturing design intent,” said Mr. Gingras. “By the time the design manager and I finished scheduling the time to use the checkers, the design engineers had already put them in the design. The design engineers simply looked at the documentation, and in a very short amount of time, instrumented the designs using the checkers. It was very straightforward.”
“We also took full advantage of the directly-inferred full_case and parallel_case checkers that Questa offers,” recalled Mr. Gingras. One of the case checkers automatically added by Questa Check detected a design error resulting from a default case item that was outside the case/endcase block. The designers used the req_ack, one_hot, maximum, value, arbiter and other checkers to specify additional important assertions about the design.
Once a design error is found, it is traditionally difficult to track down its cause. However, Questa Check enables debugging by detecting the error at the source. “As anyone who has done system verification knows, it is very difficult to isolate failures,” explained Mr. Gingras. “You may detect a failure 7000 cycles after the actual problem. If you know the checker is enabled and is there in the design, you’ll get it pretty close to where the error actually happened.”
Questa Search Finds Corner-Case Logic Error
Questa Search enhances design controllability by directly exercising cornercase behaviors. It uses dynamic formal verification technology, a combination of simulation and formal techniques, to analyze the design, stress corner cases and find bugs that directed and pseudorandom tests miss. By applying formal analysis to “amplify” existing simulation tests, Questa Search more thoroughly verifies the design without the need to write additional tests.
The delay-limiter module was identified as a verification hot spot because of its complexity, so the verification team decided to use formal verification. Rather than crafting directed tests to validate specific complex logic in the delay-limiter module, the Sun team placed checkers in the logic and used Questa Search to amplify existing simulation tests.
Using this methodology, Questa Search found an extremely subtle error in the control logic of the discard counter, which resulted in the counter being reset unexpectedly. This allowed certain transactions to be processed that should have been discarded. It was detected by an overflow checker that Questa Search triggered as it was amplifying one of the tests written by the Sun verification team. This error would have been essentially impossible to observe in simulation because its only effect was system throughput degradation due to improper bandwidth regulation; all transactions still completed successfully but the final system performance would have been reduced if this problem had not been detected.
“Questa Search found an error in the time-out logic within the design,” Mr. Gingras said. “There was a ceiling that was defined as a control status register that told you what the threshold was before you started throttling back. It turned out that the threshold was exceeded. So, we went up to that threshold and kept on going. We didn’t find that out with our traditional testing methods, but Questa Search flagged the problem immediately because we had a checker associated with it and Questa Search was able to explore that aspect of the design.”
ABV Provides the Confidence to Tape-Out
“As manager of the hardware verification group, I am constantly asked by my managers: ‘Are you ready to tape-out?’” Mr. Gingras said. “The nice thing about 0- In’s ABV Suite is: it really increased my confidence. Dynamic formal verification extends the knowledge embodied in my testbench and really goes after different aspects of the design that I hadn’t covered. That greatly improves my confidence, and I feel better when I go into my manager’s office and say: ‘OK, we’re ready to go!’”
- Lockheed Martin Space Systems Company
- Dot Hill Systems Corp.
- Xsigo Systems
- ON Semiconductor
- Institute of Microelectronics
- Evatronix IP
- National Semiconductor
- Sun Microsystems: Three-Million Gate Design
- Sun Microsystems: Multi-Clock Design
- Advanced Micro Devices
- Hyperstone: ModelSim with SystemVerilog DPI
- Hyperstone: SystemVerilog DPI
Design Verification Manager,