AMD Verifies Complex Processor and Wireless Chipsets with the Mentor Graphics O-In Verification Business Unit ABV Suite
The Dresden Design Center of AMD Saxony develops semiconductor products for wireless and wired Ethernet connectivity as well as chipsets for AMD’s processors. “Our chips are highly complex, containing control and data structures with many corner- case behaviors that occur only in very specific circumstances,” said Frank Dresig, manager of the Design/Verification Department at the Dresden Design Center.
“We increased our tape-out confidence and helped improve our time-to-market, which translated directly to project cost savings”
Advanced Micro Devices
Learn More About Questa Tools
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:
- AMD chooses Questa tools to improve verification of standard interfaces, asynchronous clock domains and control logic
- Clock domain crossing analysis finds re-converging logic after synchronization
- Assertions in simulation detect memory reads from uninitialized locations
- Formal verification discovers corner-case bug in access to shared resources
Full Range of Questa Tools Used on Two Projects
Two factors contribute to the verification complexity of the AMD chips. Since the designs usually contain multiple standard interfaces, such as HyperTransport, PCI, USB and IDE, it is critical to verify full compliance with these standards. In addition, since each interface runs on its own clock, most chips contain multiple independent clock domains. It is critical to verify that signals are synchronized correctly across each clock domain crossing (CDC).
Interfaces that must conform to standards, CDCs and complex control logic are the verification hot spots that led the AMD team to adopt assertion- based verification (ABV) to improve and accelerate their chip development process. “After an extensive evaluation, we selected the Questa® tools to improve our process by adding assertions and formal verification,” explained Mr. Dresig. The team used the Questa ABV Suite in the development of two complex products — the AMD-8111™ HyperTransport™ I/O Hub and the AMD Alchemy™ Solutions Am1772™ Wireless LAN Chipset.
Questa Checklist Verifies Clock Domain Crossings
The first project using the Questa ABV Suite was the AMD-8111 I/O Hub, part of a chipset for the AMD Athlon™ 64 and AMD Opteron™ processors. This chip connects to the host via the high-speed HyperTransport technology bus and provides connectivity to other standard interfaces, including PCI, USB, LPC, IDE and 10/100 Ethernet. Because each of these interfaces runs on an independent clock, the AMD team chose the AMD-8111 design as the focus for CDC verification.
Questa Checklist includes sophisticated CDC analysis as part of its automatic design error checks, ensuring that signals crossing between different clock domains are properly synchronized. “Questa Checklist was very easy to integrate into our overall verification methodology,” reported Mr. Dresig. The tool ran on the entire chip since the full range of interactions among the clock domains occurred only at the chip level. “The most interesting synchronization error found was a case of re-convergence, in which two independently synchronized signals were combined into the same logic”, said Mr. Dresig. “We were able to track down the problem easily, fix the synchronization, and re-run CDC analysis to verify that the error was fixed correctly.”
Designer Assertions in RTL Improve Observability
In addition to the automatic checks from Questa Checklist, the designers specified assertions in the RTL code using checkers from the CheckerWare® library. “We found it easy to understand the library and choose appropriate checkers to capture our ideas for assertions,” said Mr. Dresig. About 50 assertion checkers were added to the AMD-8111 design. The verification team also included Questa’s HyperTransport, PCI and LPC CheckerWare protocol monitors in their simulations.
“One interesting problem found by the Questa assertion checkers occurred when a prefetching bug allowed memory accesses to occur out of order,” said Mr. Dresig. When this problem happened, a memory location could be read before it was written.
“This bug was detected by a memory_access checker during our simulation tests,” added Mr. Dresig. “If we had used a pure black-box testbench approach, we might have detected this bug by seeing corrupted data on an output bus but it would have been hard to trace the source of the corruption to the memory access deep inside the chip. The assertion checkers provided greatly improved observability within the chip and allowed us to detect and fix bugs more quickly.”
Questa Search and Questa Confirm Formally Verify Key Block
Assertion specification was more widely adopted on the second project, a network controller that bridged from a PCI interface to wireless Ethernet using the IEEE 802.11b standard as part of the Am1772 Wireless LAN Chipset. “We added more than 200 assertion checkers to this chip during the development process and ran them in both block-level and chip-level simulations,” recalled Mr. Dresig.
Recognizing the limitations of simulation, the AMD team decided to use the Questa Search dynamic formal verification tool on the MAC block from the Am1772 project. “We knew that this block contained many difficult corner cases that would be hard to verify adequately with simulation alone,” said Mr. Dresig. “We found that most formal tools could not handle its size of around 100K gates of very complex logic, but that Questa Search could. It accepted our block directly, without any need for us to modify the RTL.”
The AMD engineers tagged about 10 of the assertion checkers inside the MAC block as “targets” for formal analysis, which tried to find ways to violate the targets and thereby reveal design bugs missed in simulation. About 40 temporal assertion checkers on the MAC inputs were tagged as “constraints” so that the formal analysis would consider only legal input behaviors.
Some of the control logic in the MAC provided arbitration for parallel processing elements to have fair and non-conflicting access to a set of shared resources. Since this was a verification hot spot, one of the target assertions specified by the designers checked to be sure that accesses were granted to the right resources in the right order.
“When we ran Questa Search on the MAC block, it detected a tough-to-find cornercase bug in which access to a set of shared resources was not granted in the right order,” said Mr. Dresig. “The consequences of this were quite severe — structures in the main system memory could be corrupted and, in the worst case, a system hang could occur. It is possible that we would never have found this bug with simulation alone, since it would have been very hard to set up the exact scenario from the chip inputs within our testbench.”
After this bug was fixed, the team re-ran Questa Search and then ran the deeper analysis of the Questa Confirm static formal verification tool to verify that the fix was correct. “We did not find any more design bugs and this greatly increased our confidence before tape-out,” summarized Mr. Dresig. “The Questa tools helped improve our timeto- market, which translated directly to project cost savings. As a result of these two projects, we have made Questa’s ABV Suite a part of our development methodology for new chips.”
- 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