Model Checking in Industry

  • Model checkers (most based on SMV from CMU) are beginning to be used to verify hardware designs
  • Example, RuleBase at IBM
    • RuleBase incorporates reduction techniques which automatically reduce the design size before the model checker is called
    • "Irritators" define the input assumptions to the module under test
    • Sugar is used to write properties
  • Most companies have a group dedicated to model checking
  • Electronic Design Automation tool providers are beginning to release model-checking tools