Functional verification of the z990 superscalar, multibook microprocessor complex

IBM Journal of Research and Development, May-Jul 2004 by Bair, D G, German, S M, Wollyung, W D, Kaminski, E J Jr, Et al

This paper describes the verification methods and techniques that were established to verify the microarchitecture and architectural correctness of the z990 microprocessor and storage subsystem. The ring-based, four-book storage subsystem links 64 superscalar microprocessors together in this system. The verification process started at the unit level, which focused on the correctness of the microarchitecture, and then proceeded to the element level to verify the architectural correctness of the microprocessor and storage subsystem. After successfully completing element stress testing, the components were combined and verified at the system level. Since the methods used at system-level verification were much the same as the ones used on the CMOS-based IBM S/390� Parallel Enterprise Server G4, the focus of this paper is on the work done at the unit and element levels.

Introduction

A major logic verification effort was required to verify the functionality of the z990 superscalar, multibook microprocessor complex. The verification team developed and executed a staged verification plan based on a broad range of verification technologies and collaborated with the logic design team to formulate the verification plan to ensure that all features of this complex system were fully verified.

To successfully verify this design point, the verification team built on the hierarchical verification approach used on the CMOS S/390* Parallel Enterprise Server G4 System [I]. For this system, the verification effort began at the protocol level using an abstract model. It then continued at the designer level, subunit level, unit level, multiunit level, element/chip level, and finally system level. The abstract protocol model, using a formal verification tool called the Murphi Verifier, allowed the team to verify the multibook protocol before the design was committed to a hardware description language (HDL). All major units in the microprocessor were first verified in a unit simulation environment. Subunit and multiunit simulation environments were created as necessary to fully stress the microarchitecture.

The verification team included a core of expert verification engineers who were responsible for setting the direction of the different simulation environments. These experts would select the simulation logic boundaries as well as the verification technology used to verify a particular piece of the design point. Both proven verification technologies and new, leading-edge techniques were used to verify this complex design point. There was no set formula to determine which technology to use for a given environment. The verification techniques from which the team of experts selected included the following technologies: Murphi Verifier, extended coverage models, asynchronous clock modeling [2], random command-driven techniques, architectural test-case generators, system reset verification, disabled or degraded configuration verification, recovery verification, and performance verification techniques.

Formal verification of the memory ring protocol

Figure 1 illustrates a four-book z990 system. Each book contains processors (P), a section of main memory (Mem), an L2 cache (L2), and a system control (SC). The books send and receive messages on a bidirectional ring. When a processor issues a memory request that cannot be satisfied locally within the book, the SC sends messages to the other books on the ring. The messages that flow on the ring and the rules for processing these messages form the memoiy ring protocol.

Because the memory ring protocol for the system was a new design with many novel features, the design team considered it important to formally verify the protocol. Over the course of the project, the formal verification process revealed a number of crucial problems, which led to major changes in the design of the protocol. Significantly, most of these problems were not detected in the course of random simulation of the logic-level implementation.

The general method for analyzing a complex protocol, such as the z990 ring protocol, is to create an abstract protocol model that can be checked by systematically examining all of its reachable states. There are two reasons why the team needed to use an abstract model instead of attempting to formally verify the logic-level implementation of the protocol. First, the logic-level implementation was much too large to formally verify by current methods. To check the correctness of the z990 ring protocol, the team had to show that when the four books interacted on the ring, no errors could arise from the interaction. While the logic-level implementation of the four books was much too large to verify formally, a protocol model of the four books was small enough to be fully analyzed. The second reason for building a protocol model was that it allowed the designers to check the correctness of new protocol features before implementing them. The team found that this ability saved them valuable time in the design project.