Hardware verification is typically performed by a combination of simulation and formal verification. While simulation is still its major component, formal verification's importance is growing and often represents an important part of the process. In contrast to simulation, which can only increase confidence over the design's correctness, formal verification has the ability to comprehensively prove this correctness. Due to size and time complexity, formal verification application is limited to appropriate areas, but technological advances have now enabled its usage in an almost pervasive way. In the Formal Verification and Quality Technologies group, we are developing formal verification technology, and verification tools which rely on this technology. Our main and flagship project focuses on the development of our state-of-the-art model checker called RuleBase SixthSense Edition. Another project involved developing a tool called Diver, for designer-level verification, which employs both formal verification and simulation capabilities. Finally, a technology for analysis and verification of design resiliency to soft errors is being developed as part of the InsightER project. These three projects are described in more details below.


Manager

Eli Arbel, Manager Formal Verification and Quality Technologies, IBM Research - Haifa

RuleBase SixthSense Edition

RuleBase SixthSense Edition

RuleBase SixthSense Edition represents the third generation of successful formal verification technology in IBM. The tool combines powerful property checking capabilities with advanced sequential equivalence checking technology and a unique transformation-based verification framework.

Diver

Diver

The widening verification gap forces VLSI teams to reconsider existing methodologies and processes. An emerging trend is breaking the traditional partitioning between design teams and verification teams, making designers more involved in the verification process of their own code.

Soft Error Verification

Soft Error Verification

Soft errors are transient bit-flips caused mainly by cosmic radiation, package radioactivity, or signal integrity issues--and can contribute to performance degradation and silent data corruption. We develop tools to help ensure that reliability requirements are properly met, especially in high end systems running mission-critical applications.

Quantum Circuit Simulation

Quantum Circuit Simulation

As part of the global development effort of IBM Q, IBM’s quantum computer, and the related software stack QISKit,we develop and analyze approximate noise models to better understand the behavior of quantum algorithms when run on noisy (i.e., non-fault-tolerant) quantum machines. These also serve as efficient, realistic reference models for the hardware.

IBM Functional Coverage Unified Solution (IBM FOCUS)

IBM Functional Coverage Unified Solution (IBM FOCUS)

IBM FOCUS is an advanced test planning tool to improve the testing of applications. The tool uses Combinatorial Test Design to generate an efficient test plan, providing consistent coverage across the test space at a known depth, while significantly reducing the required resources.