Formal Verification Technologies
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 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.
While our main focus is on Formal Technologies, we have also a project in the area of HW/SW co-verification. It is targeted to the formal definition and modelling of pervasive sequences, and is described at the bottom of this page.
RuleBase SixthSense Edition represents the 3rd generation of formal verification technology in IBM. The tool combines strong property checking capabilities along with advanced sequential equivalence checking technology and a unique transformation-based verification framework. These capabilities originated in the two former IBM FV tools, namely RuleBase Parallel Edition and SixthSense. Altogether RuleBase SixthSense Edition supersedes its two predecessors in terms of capacity and is the most powerfull formal verification tool ever made by IBM.
RuleBase SixthSense Edition is used intensively by IBM verification engineers and logic designers, as well as by several external customers. It offers a full-fledged support for VHDL, Verilog and SystemVerilog HDL languages, along with excellent PSL and SVA property specification language capabilities.
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.
Diver is built to be an easy-to-use, yet very powerful tool for designer-level verification. With Diver, logic designers are able to exercise various levels of verification-related tasks on their logic blocks, ranging from initial design exploration to complex bug hunting. Diver does not require learning a new verification description language but rather provides an intuitive graphical user interface for specifying design behavior and expected results.
Soft errors are transient bit-flips mostly caused by cosmic radiation, package radioactivity, or signal integrity issues. While not indicating a permanent hardware defect, soft errors may still be hazardous to the design with their effect ranging from possible performance degradation to silent data corruption. As resiliency against soft errors is important, especially in high-end systems running mission-critical applications, tools and methodologies to effectively ensure that reliability requirements are properly met are needed.
In this activity we are developing a technology aimed at assisting design and verification teams in their reliability analysis and verification tasks. The goal is to have a tool which is able to accurately quantify chip reliability and point at logic areas which need to become more robust in order to meet the given chip reliability requirements.
We also work on a solution to a growing problem of pervasive hardware and software verification. More specifically, the team explores and develops new model-based approach for implementation of pervasive code sequences and procedures. These sequences, which are part of a system firmware code, are responsible for a variety of highly important processor functions that are complimentary to a regular processor functionality such as boot process, power on/off, power management, unit and block management, etc. This highly innovative approach will allow hardware and software development teams to formally model the relevant aspects of the pervasive logic and the corresponding firmware code to facilitate their co-design and co-implementation. We aim to develop a technology that will enable model-based generation of actual pervasive sequences and procedures code, their system configuration dependent variants, behavior simulation models for pervasive hardware, and testcases for hardware and software verification purposes.