Property Proving with an Invalid Property

This example shows how to find an invalid property using Simulink® Design Verifier™ property proving analysis. It attempts to prove that when the sum of the current and six previous input values is greater than 6, the output equals 2. In this case, the property is invalid because a single large input value (e.g. 255) causes the sum to be greater than 6. Simulink Design Verifier produces a counterexample that demonstrates the violation.

open_system('sldvdemo_debounce_falseprop');