To open the Simulink®
Design Verifier™ block library, at the MATLAB® command
The Simulink Design Verifier block library has three categories of blocks:
Objectives and Constraints — Blocks that define custom objectives and constraints
Temporal Operators — Blocks that define temporal properties on Boolean signals
Verification Utilities — Miscellaneous verification utilities
The block library also has a sublibrary, Example Properties, that includes examples of how to specify common properties in your model. You can easily adapt these examples for use in your models.