IBM®
Skip to main content
    Israel [change]    Terms of use
 
 
 
    Home    Products    Services & solutions    Support & downloads    My account    
IBM Research

RuleBase Parallel Edition

Formal Verification


Generalized Buffer (PSL/Sugar version)

Getting Started

To complete this tutorial, you need to:
  • Read the user manual and complete its tutorial
  • Own a RuleBase license
  • Obtain the appropriate files (see installation)
  • Create your own set of envs (for the environment) and rules (for the rules) files

You may rename the two original files (which were provided within the tutorial.tar), and you may also create your own envs and rules files. If you do so, place them in the same directory.
If you decide to run the rules without re-writing them, you may use the original files.

The rules file must be included in the envs file. A typical envs file starts with:
#include "rules"
To check that you have everything you need, write a first rule (in the rule file). A sample rule is:
vunit tauto
{
  "This rule just checks that 1 is always true"

  assert 
    always (1);
}
If you made changes in both the envs and rules files, refresh the rule list by selecting Rule -> Refresh Rule List from the RuleBase PE menu bar. After refreshing the rule list, you can run the "tauto" rule with RuleBase/PE.

After running the "tauto" rule, click the "Formulas" entry. Your RuleBase/PE main screen should look something like this:

Click to see full size
  Click to see full size



 
 





    About IBMPrivacyContact