Verification Technology (Computer Systems Design sub-discipline) - Awards

Verfication Awards


Research Contributions to STG Hardware Verification

Functional verification of modern hardware design today consumes roughly 70% of the effort invested in the design cycle. Throughout the last 25 years, Research played a major role in enabling STG's hardware competitiveness through innovative verification technology. The Research team invented and developed an impressive set of state-of-the-art technologies, which provided IBM with a significant competitive advantage in the marketplace. In addition, Research influenced the relevant industry in dramatic ways, clearly initiating several revolutionary changes in how verification is done today, within IBM and throughout the industry. By these achievements, the verification team in Research has acquired a leading role in the industry, accompanied by strong recognition in the Academia.

Research's innovative hardward verification assets span the entire range of verification tools and disciplines:

  • Test Generation technologies (RTPG, Genesys, Genesys-Pro, X-Gen and FPgen)
  • Formal Verification technologies (RuleBase, RuleBase PE)
  • Checking (PSL, Protocol verification)
  • Functional coverage technological assets

Main transformational influences:

  • pioneering the concept of expert systems for pseudo-random test generation
  • introducing the first industrial-strength formal verification model checker

Contacts for more information about this accomplishment

  • Moshe Levinger/Haifa/IBM


Threadmill - Exerciser for Post-Silicon Validation

Threadmill is a bare-metal micro-processor-exerciser that enables a unified functional verification methodology. It leverages a uniform test-case control from pre-silicon simulation, acceleration, and emulation through the testing of actual silicon.

Research commenced Threadmill exerciser development in 2006, and it quickly matured into a project in deployment in the p Series processor verification. It is designed to enable the continuation of the pre-silicon verification methodology on the Awan accelerators as part of the Exerciser on Accelerators (EoA) effort and the bring-up lab on silicon. None of the other bare-metal tools possess similar capabilities.

Threadmill provides a methodological approach (extending the pre-silicon methodology onto acceleration and silicon) and added value compared to other post-silicon tools, such as fine-grain control over threads and thread irritation. It allows looking for hardware bugs in a new way that was not possible before through randomly seeded or formal methods. Threadmill was used during the POWER7, POWER7+ and POWER8 development process for processor verification and validation.

Contacts for more information about this accomplishment

  • Ronny Morad/Haifa/IBM
  • Laurent Fournier/Haifa/IBM


X-Gen - Automatic Stimuli Generator for System Level Verification

(Outstanding - upgraded from 2004)X-Gen, an intelligent stimuli generator for functional verification of hardware systems, allows higher quality verification and shorter hardware verification cycle. This enables IBM to innovate in system designs and to compete in an industry where time to market is decreasing all the time. X-Gen, compared to the previous state of the art, is able to cope with very large systems (thousands of threads), heterogenous processors and accelerators in a single simulation environment.X-Gen has become the de-facto standard exclusive system-level stimuli generator for all Power systems(P4,P5/+,P6,P7/+,P8), all gaming systems (Xbox360, Playstation3, Wii), all zSeries systems (z9, z10, zGryphon/+), I/O coupling protocols and PRISM. X-Gen has revolutionized the way system verification is done by allowing the porting of IP from one system to another; this is allowing higher quality verification of these designs with significantly fewer resources.Research invented, developed, demonstrated, coded, debugged, documented, delivered and supported X-Gen. This outstanding functional verification tool employs AI technologies (constraint satisfaction problems and knowledge representation) to generate sophisticated system-level stimuli that target hard-to-reach corner cases using system-wide interfaces. In addition, it provides OOP constructs in its system-level input language to facilitate reuse and cost reduction.Contacts for more information about this accomplishment

  • Ronny Morad/Haifa/IBM


Genesys-Pro: Test-Program Generator for Functional Verification of Processors

Genesys-Pro is a model-based random test-program generator for the functional verification of processors. Research's methodology for Genesys-Pro uses two distinct languages: one that describes the system under test and another for describing test specification.  The modeling language contains a limited set of high level declarative constructs representing architectural concepts. These constructs are automatically translated into constraints and solved to generate stimuli. A general purpose object oriented procedural language is only used to complement the declarative modeling when it is not expressive enough.

Genesys-Pro technology allows systematic and large-scale reuse of verification knowledge in many projects, many sites, and along many years. It allows quick reaction to architectural and design change, is very efficient in using verification engineers' time and skill, and allows massive generation of high quality stimuli. Since 2000, Genesys-Pro has been used as the major verification means for functional verification of all IBM PowerPC processor designs. In all these designs, Genesys-Pro has been widely deployed for unit-, core-, chip-, and partially for system-level verification. It has contributed to uncovering the majority of core-level functional bugs in these designs and was crucial for their timely completion.


RuleBase Parallel Edition - A Parallel Formal Verification Platform

Research converted a model-based formal verification software package called RuleBase to a parallel configuration called RuleBasePE. The new tool, which formally checks design of logic at the block and unit level, can be applied to more complex designs, resulting in shorter development times and significant cost savings.

Research has continued to improve the software, which is now capable of formally verifying hardware chip designs with orders of magnitude greater complexity. RuleBasePE is now used in various verification steps in all of IBM's chip designs and is even licensed to non-competing companies.

Contacts for more information about this accomplishment

  • Sivan Rabinovich/Haifa/IBM


Contribution to Formal Verification of STG Processors

IBM's high-end processors are used in many servers, workstations, and super computers that IBM manufactures. Functional hardware verification checks that the processors' design conforms to a given specification and has no defects. Formal verification (FV) is a static verification method that mathematically proves that a design complies with a given set of properties. IBM's processors pose a great challenge to verification, and to FV in particular, because their design is optimized for performance.

In recent years, a Research team has significantly contributed to FV of the IBM's processors. The FV Application Team verified dozens of design blocks and uncovered hundreds of design flaws that could have caused serious faults, such as hang-up or major performance deterioration. The team has developed and applied multiple innovative methods that allow efficient verification of significant portions of the design and quickly uncover defects that were undetectable before.

Contacts for more information about this accomplishment

  • Sivan Rabinovich/Haifa/IBM


Test Generation Solution for zSeries Processor Verification

The System z processor cores are at the heart of System z differentiation. In each generation, new architecture extensions are implemented. At the same time, a shift to more complex micro-architectures was required to allow System z to remain competitive in the new workloads demanded by customers.

Test generation technologies play a key role in ensuring the processors are functionally verified quickly, efficiently and thoroughly. The z196 core was the first out-of-order System z design. From the start of the project, it was clear that legacy core level test generators were not fit to address the new complexity induced by the new design point.

Research developed a new test generator called zPro to address the System z specific needs. It is based on the Genesys-Pro platform which has been used by the System p servers and other Power designs for many years . This technology proved to be a key enabler of the z196 project success and the future development of the System z roadmap. The technology was developed in collaboration with the STG EDA team and with strong endorsement by the z196 core verification team.

Contacts for more information about this accomplishment

  • Oz Hershkovitz/Haifa/IBM