 |
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
|
Hardware Verification
- Application of formal techniques to chip designs
|
Slide 19 of
30 |