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.
| 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
