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