RuleBase Parallel Edition

Basic Features

1. Powerful standard specification language (PSL)
   • Facilitates easy formulation of complex temporal properties.
2. Convenient modeling of input constraints (PSL, Verilog, VHDL and GDL flavors)
   • Enables easy abstraction of the environment behavior.
   • Eases management of multiple environment configurations.
3. Powerful model checking algorithms
   • BDD-based, SAT-based; efficient exhaustive search, partial search, and adaptive search.
   • Parallel state-space search.
   • Refer to the advanced algorithms page for more details.
4. Automatic state space reductions
   • Cuts down model size while retaining functionality.
   • Leaves only parts relevant to verified formulas.
5. Generation of counter-examples as timing diagrams or simulation testcases
   • Counter-examples are provided as timing diagrams.
   • Counter-examples can be translated to test programs.
   • Supports generation of VCD format.
6. Convenient control over the process
   • Highly automated.
   • Supports manual runtime intervention.
   • Easily configurable to work with a network job scheduling system, like LSF and Condor.
7. Debugging aids
   • Vacuity detection performs sanity check on your specification.
   • Witness generation shows meaningful traces that follow your specification.
8. Smooth integration with design flow
   • Verilog and VHDL are supported via an IBM compiler ("Portals").
   • VHDL is also supported via Synopsys Design Compiler (DC license required).
9. Platforms
   • IBM: RS/6000 running AIX.
   • Solaris.
   • Linux Kernel, Red-hat.
   • For details regarding versions, please ask your contact person in the IBM RuleBase group.

10. Friendly GUI

    • Supports vunit/project configuration.
    • A single GUI controls jobs on different machines.
    • And much more ...