RuleBase Parallel Edition
- Powerful standard specification language (PSL)
- Facilitates easy formulation of complex temporal properties.
- Convenient modeling of input constraints (PSL, Verilog, VHDL and GDL flavors)
- Enables easy abstraction of the environment behavior.
- Eases management of multiple environment configurations.
- 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.
- Automatic state space reductions
- Cuts down model size while retaining functionality.
- Leaves only parts relevant to verified formulas.
- 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.
- 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.
- Debugging aids
- Vacuity detection performs sanity check on your specification.
- Witness generation shows meaningful traces that follow your specification.
- 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).
- IBM: RS/6000 running AIX.
- Linux Kernel, Red-hat.
- For details regarding versions, please ask your contact person in the IBM RuleBase group.
- Supports vunit/project configuration.
- A single GUI controls jobs on different machines.
- And much more ...