Мне нужно проверить это требование
Сигнал Serial_in_FF2_meta_out фильтруется по импульсам короче двух тактовых периодов Serial_CLK и передается в Serial_out по переднему фронту CLK_int после 3 импульсов Serial_CLK.
Как вы видите, у меня есть два часа здесь, я написал это:
property Rx_Filter_V3_5_1;
@(posedge Serial_CLK )
disable iff(!RST_in)
(Enable) and (Serial_in_FF2_meta_out)[*2] |=> ##3 (Serial_out === $past(Serial_in_FF2_meta_out,3));
endproperty
DS_3_4_31_5_1:
assert property(Rx_Filter_V3_5_1);
cover property(Rx_Filter_V3_5_1);
Проблема здесь после 3 импульсов Serial_CLK, симулятор ждет другого переднего фронта Serial_CLK (так как мне нужен оператор импликации не перекрывающихся) для проверки.
ну, я думаю, что это нормально, потому что я определил @pos Serial_Clk, мне нужно, чтобы симулятор проверил нарастающий фронт CLK_int, а не Serial_CLK
Примечание: я не могу установить уравнение между двумя часами, так как частота Serial_CLK изменяется