В этом примере показано, как выполнить проверку свойств Simulink Design Verifier с помощью блока Proof Absulation. Он пытается доказать, что, когда сумма текущих и шести предыдущих входных значений больше 6, выходной сигнал равен 2. Модель включает блок Proof Summission, ограничивающий ввод 0 или 1. Simulink Design Verifier ищет нарушения на 20 или менее шагов времени. Он не может найти нарушение, поскольку свойство является действительным в предположении.
open_system('sldvdemo_debounce_assumeblk');
