Our specialty covers the verification and testing of hardware and software systems. The focus of our work spans functional verification of hardware, quality assurance of software and the cloud stack, quality of AI algorithms, and verification aspects of quantum computing.
Our expertise is built upon a strong legacy of high-quality research and development going back over 30 years, during which we pioneered several of the practices currently prevalent in the industry. Some of our prominent technologies include:

  • Using constraint-solving capabilities for stimuli generation in the domain of functional verification of hardware. This includes separating the architecture description (model) from the generation engine.
  • Scalable formal verification technology that employs state-of-the-art model checking algorithms with extensive support for all common design and specification languages, including PSL (an IEEE standard specification language conceived by our department).
  • Powerful post-silicon validation aimed at finding intricate bugs that occur in complex multi-processing scenarios or under advanced memory management constraints, such as transactional memories.
  • Advanced Combinatorial Test Design (CTD) technology that dramatically reduces the number of tests required to achieve a desired level of parameter interaction coverage over the test space of the program or system under test.
  • Analytics framework to provide insights on Big Data collected during the verification/testing process, enabling better decision making in the verification process.

Our primary clients within IBM are IBM Systems and Global Business Services. Many of our tools which are used internally are generic and are used by external clients as well.

The technologies developed in our department have received multiple IBM awards. Our overall contribution to IBM’s hardware development was awarded an IBM Research Extraordinary Accomplishment, the highest rank for technical accomplishment awarded by IBM Research. Our CTD technology was awarded an IBM Corporate Award, the highest award granted by the IBM corporate.

In our ongoing endeavor to develop the next generation of verification technologies and capabilities that can meet the increasing needs of our customers, we are exploring new exciting directions, including:

  • AI Quality: Technology and methodology to assess the quality of successful machine learning solutions. This includes advanced bias and drift detection techniques.
  • Quantum Computing: Enhancing IBM Q through the Qiskit open source framework with simulation engines which consider various quantum noise models and with verification and characterization capabilities for quantum software and hardware.
  • Cloud Quality: Tools to verify network policies, test functional quality, and check and ensure the resiliency of IBM cloud.
  • Performance Verification: Techniques to help verify that a given design meets its performance requirements.


Sharon Keidar-Barner, Manager Verification & Quality Technologies, IBM Research - Haifa