Skip to main content

The IBM Formal Verification group develops formal verification solutions for industrial use. Our main asset is RuleBase SixthSense Edition, an industrial strength formal verification platform.

  • RuleBase SixthSense Edition has been used to formally verify designs in IBM for almost two decades. It is used daily on the hardware projects developed across IBM, running on different design types of different sizes, with different proof algorithms.
  • RuleBase SixthSense Edition is also available outside of IBM through a licensing process governed by IBM Research. Please contact Eli Arbel for more details on licensing.

Our global team of formal verification experts is pushing the limits of the technology to make RuleBase SixthSense Edition the strongest tool available on the market. The tool is constantly evolving with the addition of cutting edge technology.

RuleBase SixthSense Edition has a simple intuitive interface that makes formal verification accessible to any verification engineer. In IBM and many other companies, formal verification is quickly becoming an inseparable component of the verification flow.

RuleBase SixthSense Edition User Interface

Screen shot

Why Formal Verification?

Simulation used to be the only way to carry out pre-silicon verification. As hardware design complexity grows and the late detection of bugs becomes more expensive, formal-verification (FV) solutions have become a necessity in every hardware design center.

Using adequate FV methodology ensures that a design-under-test is bug free. FV has a fast set up environment and can easily reconstruct bugs that were found in the lab.

What is RuleBase SixthSense Edition

For almost two decades, RuleBase SixthSense Edition has been used by IBM and other companies to formally verify the most critical portions of their hardware designs. IBM's mainline processors, IBM's gaming processors, and many other hardware designs were extensively verified by RuleBase SixthSense Edition. The following make RuleBase the ultimate solution for formal verification:

  • Power, power, and more power. The strongest formal solution out there.
  • Ability to handle the largest pieces of logic with the fastest run times.
  • Support for ABV in the popular assertion languages PSL, SVA.
  • First on the market with the most powerful model checking algorithms.
  • Easy to use, easy to implement in an existing verification flow.
  • Comprehensive package includes everything (compilers, wave viewer, easy GUI, etc).
  • Personalized customer support.

From Automated Expert mode to a Full-Control Mode

There is no single model checking algorithm which can effectively solve all verification problems. Hence having a reach portfolio of algorithms is key in enabling a formal verification tool to successfully cope with problems of various types, sizes and complexities. RuleBase SixthSense Edition includes a reach set of model checking algorithms (called engines) which run in a transformation-based verification framework (TBV). The TBV framework enables transferring a given model checking problem from one engine to the other while gradually simplifying the problem until it is completely solved. In order to facilitate efficient utilization of the reach set of engines avialable in RuleBase SixthSense Edition, a special Expert Mode engine is available which automatically orchestrates the use of the various engines in a given run. For experienced users a manual mode is also available, in which users build their own configurations of engines using a GUI based configuration manager. A set of pre-defined configurations, each tailored for specific verification scenario (e.g bug hunting) are also provided.

Screen shot

Screen shot