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