Skip to main content

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 three separate technologies. Our main and flagship project focuses on the development of our state-of-the-art model checking technology, RuleBase SixthSense Edition. We are also developing a tool called Diver for designer-level verification. Finally, the SER project concentrates on the verification and handling of soft errors. These three projects are described in more detail below.

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.

There are several techniques that can be used by designers in the process of functional design verification. One approach is to embed properties in the design or create a verification environment, using simulation or formal analysis tools to verify the written properties with further inspection of a counter example for analyzing the problem. However, while assertion-based verification improves the overall quality of the design, it requires a certain level of design code maturity and expertise in verification. Another approach is to use test generation and simulation techniques. Despite high expressiveness in describing various random scenarios and expected design behavior, this approach requires a heavy investment in a project setup and building an environment.

As it becomes necessary to provide a technique for easy design exploration and verification on a block level, before the complicated formal/simulation environment is ready, there's a need for an easy, interactive tool that allows a quick entry into the design exploration. Diver is a graphical tool intended for designer-level verification. It provides designers with an easy interface for simulating their RTL under selected prime scenarios. The simulation process includes specifying input stimuli patterns, clicking the Simulate button, and analyzing the results appearing as a timing diagram.

Diver goes beyond simulating just input patterns. It also allows designers to specify scenarios in term of internal events or output events, and then find the input patterns that can make these events happen. For that purpose, Diver interfaces with a formal analysis tool. Having such a tool under the hood will also allow designers to go as far as assertion-based verification.

Soft Error Verification

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 due to excessive machine restarts, to silence data corruption, where computation integrity is violated unnoticeably. Major areas of focus in the landscape of high-end microprocessors are data integrity and long mean time between failures; hence the need for effective tools and methodologies to ensure that reliability requirements are properly met.

As part of this activity, a tool called InsightER is being developed to help design teams achieve their hardware reliability requirements more easily. InsightER (Insight on Error Rates) works on a pre-silicon input (RTL), offering analysis capabilities and feedback on reliability characteristics early in the design cycle. Soft error analysis and mitigation occur at various levels of abstraction, starting from the device (transistor) level up to the application and system level. InsightER performs analysis on the logic level (VHDL/Verilog) and encompass reverse-engineering-like capabilities to extract information regarding existing (or the lack of) error detection and correction mechanisms in the hardware itself. The tool includes static analysis methods, such as structural identification of known error-detection mechanisms, as well as formal-based methods for verifying that existing error-detection and correction mechanisms are properly implemented.

InsightER is already deployed in various server design projects in IBM, and was successfully used in several System z programs and server ASIC chips. As we move forward with developing InsightER technology and methodology, more automated techniques are being developed that will facilitate the use of the tool in future projects. Our ultimate goal is to provide a reliable sign-off-quality analysis tool that can be seamlessly used on internal IBM designs as well as on external vendor chips with minimal manual effort.

Design Methodology

With the growth in complexity of processor designs, the number of functional bugs grows beyond the capability of verification to handle. We are seeking to improve the logic design process so that the design is created with less functional bugs.

Manager

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

: Manager Formal Verification Technologies, IBM Research - Haifa