Skip to main content

RuleBase Parallel Edition

Formal Verification

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 ...