Property Proving Workflow for Fixed-Point Cruise Control with Block Replacements

This example shows how to prove properties in a fixed-point cruise control algorithm. It references the design model using model reference so that the original design model is unchanged. A block replacement rule specifies the property that checks if an overflow is possible. The verification subsystem specifies an assumption on the range of the speed input during property proving. This model configures Simulink Design Verifier to apply a block replacement to the Sum block that feeds the outport of the fixed-point PI Controller in the referenced model and return a counterexample that demonstrates an overflow.

open_system('sldvdemo_cruise_control_fxp_verification');