Skip to main content

RuleBase Parallel Edition

Formal Verification

Overview

RuleBase PE is IBM’s industrial-strength platform for hardware formal-verification, and is  developed in the IBM Haifa Research Lab. RuleBase is especially applicable for verifying the control logic of large hardware designs.

RuleBase PE offers formal-verification technology to designers and verification engineers. Its use is not limited to experts and requires only a short training period.

RuleBase PE offers an “automatic-pilot” mode for novices and a “manual gearbox” mode for senior FV engineers—checking  both black-box and white box properties of a design.

What's new in RuleBase version 2.05?
More powerful SAT-based verification engine
New abstraction algorithm
Efficient model-size reduction engine
New semi-formal search capabilities
Smarter utilization of parallel computing
Clear vacuity explanation
Enhanced user interface
Productivity tool to reduce environment setup time

Why Formal Verification?

Simulation used to be the sole technique of pre-silicon verification. As hardware design complexity grows and late detection of bugs becomes expensive, formal-verification (FV) solutions 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 PE?

For over a decade, RuleBase PE has been used by IBM and other companies for formal verification. In fact, IBM’s mainline processors were extensively verified by RuleBase.

  • Verifies large design segments.
  • Perfectly supports PSL. 
  • Includes superb customer support
  • Provides deadlock-free proofs - including full proof and witnesses
  • Supports liveness properties