A truly extraordinary accomplishment
Research verification work receives Extraordinary Accomplishment for improving STG productivity and competitiveness
During the last two decades, assets developed by IBM Research – Haifa have served as vital verification tools for over 100 major IBM hardware programs. These innovative technologies saved over $500M for STG, by enhancing quality and reducing the time and personnel required to find bugs before hardware goes out.
Is the computer always right?
The computer doesn't make mistakes—or at least that's what people say. Computer chips and systems control everything from our phones, fridges, and Xboxes to trains, planes, and power plants. But what process makes sure the chip or system is bug free? Verification, or the process of making sure things work as intended, is critical to any component or system. In fact, the functional verification of modern hardware design consumes roughly 70% of the effort invested in the design cycle.
Researchers in Haifa, Israel have spent nearly three decades delivering breakthrough technologies in the area of test generation, formal verification, and test coverage. This year, the Haifa team was awarded an Extraordinary Accomplishment for helping STG competitiveness through the large collection of verification assets developed over the years.
Receiving an extraordinary accomplishment is an exceptional and unique event, noted Oded Cohn, director of IBM Research – Haifa. Although our lab is well-known as a world center of competence in the area of verification, it is exciting to be recognized as having revolutionized a field of science and contributed so greatly to an IBM business.
Research assets in verification
Verification assets designed at the lab include such developments as the property specification language known as PSL, which is now an IEEE industry standard; automated test generation to improve the quality of final products; the first-ever industrial strength tool for formal verification; and the use of constraint satisfaction in test generation.
"These are very smart technologies that find bugs and are easy to use—so you don't have to learn a lot to enjoy the benefits," explained Moshe Levinger, senior manager of verification technologies at the Haifa lab. "We were awarded the Extraordinary Accomplishment based on our long-term relationship with STG, helping them improve productivity, cut costs, and enhance the quality of chips."
The researchers in Haifa are continuously working to increase the automation associated with verification tasks, so that bigger designs can be verified faster and more reliably. The various teams have helped shaped the industry over the years by developing complex mathematical modeling techniques, promoting new standards in verification, and introducing novel methods for automation and increased coverage. The end result is a collection of verification assets that help IBM and its clients improve the quality of the final product and reduce manufacturing costs—without trading off one for the other.
"We're not going to stop forging ahead just because we got to the top," explained Levinger. "We need to continue moving ahead to stay competitive in the market and keep up with changing technologies. The potential and challenges only grow with time."
Staying in the lead
The teams are already working on new frontiers in verification, including adapting verification methods previously used for hardware and applying them to the software domain. One example is a project that uses formal verification to make sure healthcare insurance providers correctly revise, or 'translate', their claims processing to accommodate new standards and regulation. The IBM system verifies the translation is done accurately and the semantics have the same meaning they did before being moved to the new standards. In another project, verification techniques are used for nuclear power plants to test that the software upgrades planned work correctly before the system is upgraded to the new version. Researchers are also working with the XIV unit in IBM, to help verify the correct functioning of a complex new storage software protocol critical to the correctness of the entire storage solution. Many of these projects verify software using techniques originally developed for hardware components.
According to Levinger, IBM's verification leadership stems from the broad scope of assets developed and the capacity of those assets to verify such a wide variety of components. "It's about many innovative technologies developed by many talented individuals—that's the secret to success."