Main Content

Specify and Verify Design Requirements

Verify design against requirements, refine counterexamples by using input assumptions

Safety requirements define undesired behaviors in a model. Simulink® Design Verifier™ uses property proving to verify that properties associated with model requirements hold under all possible input values or provides counterexamples that lead to violations. You use Simulink Design Verifier to model design requirements as properties and then Prove Properties in a Model.

Blocks

expand all

Proof AssumptionConstrain signal values when proving model properties
Proof ObjectiveDefine objectives that signals must satisfy when proving model properties
AssertionCheck whether signal is zero
DetectorDetect true duration on input and construct output true duration based on output type
ExtenderExtend true duration of input
ImpliesSpecify condition that produces a certain response
Within ImpliesVerify response occurs within desired duration
Verification SubsystemSpecify proof or test objectives without impacting simulation results or generated code

Functions

expand all

sldv.assumeProof assumption function for Stateflow charts and MATLAB Function blocks
sldv.proveProof objective function for Stateflow charts and MATLAB Function blocks
sldvextractExtract subsystem or subchart contents into new model for analysis
sldvoptionsCreate design verification options object
sldvrunAnalyze model
sldvreportGenerate Simulink Design Verifier report

Topics

Start Here

Requirements Modeling for Verification and Validation

Verification by Property Proving