Skip to main content

RuleBase Formal Verification Tool Now Available on More Platforms

Runs with enhanced performance on Linux, Sun/Solaris, and AIX

Select a topic or year

Haifa, Israel - 23 Jun 2002: The Formal Methods department at the IBM Research Labs in Haifa has released a new version of RuleBase, the industry-leading model checker. As a functional verification tool, RuleBase determines whether a design (typically a chip design) functions according to a specified set of properties.

These tools help verification engineers create mathematical models of chip designs. The tools then apply mathematics to check the model and ensure that the design actually does everything it was supposed to do, as per the specifications that were stated in the original architecture.

The tool ensures a very high degree of verification coverage and design quality, as well as faster time-to-market for the final design. As opposed to simulation, RuleBase employs static checking algorithms and requires no test cases. To date, RuleBase supports assertion-based verification (ABV) methodologies across IBM and for several strategic business partners. ABV lets verification engineers specify assertions about required behaviors of the design. RuleBase can then detect whether these assertions are ever violated - which amounts to finding "bugs" in the design. Assertions can also reference internal signals that are not always propagated to design outputs, and in this way identify problems that random simulation alone would not. Many design teams have reported that RuleBase detected design flaws that would have escaped traditional simulation methods.

RuleBase 1.4 comes in two versions: RuleBase Classic and RuleBase Premium. The heart of the Classic offering is a binary decision diagrams-based search engine called Discovery, which has been in use since 1994 and is continuously being improved by IBM Haifa's Formal Verification group.

The Premium version of RuleBase 1.4 is now officially available to the verification community. On top of the Classic version, RuleBase Premium contains a set of additional verification engines, which excel in finding bugs in very large, high-complexity logic models.

Similar to previous versions, RuleBase 1.4 runs on both AIX and Solaris, and now runs on Linux.

RuleBase 1.4 highlights:

Appendix: Training Sessions, 2002
RuleBase classes may be opened in the Q3-Q4/2002 timeframe at the IBM Research Labs in Haifa, based on user requests. These classes come in two flavors: Introductory and Advanced.

The duration of the Introductory RuleBase Class is 2 days, and the covered material includes fundamentals of formal verification and model checking, the Sugar specification language (including the modeling of input constraints), and handling size problems.

The duration of the Advanced RuleBase Class is 3 days, where the covered material includes advanced modeling (sequential processes, design overrides, and use of restrictions, assumptions and hints), liveness and fairness considerations, RuleBase flow management, advanced options, the Reduction Analyzer, and a special chapter on Sugar 2 and its effect on using RuleBase.

Classes fill up quickly and are limited in capacity. For further information, please send the following information ASAP to Gil Shapir (

Related XML feeds
Topics XML feeds
Chemistry, computer science, electrical engineering, materials and mathematical sciences, physics and services science