Утверждение для проверки сбоя в сигнале

Допустим, есть сигнал a. Когда сигнал становится высоким, он должен оставаться высоким как минимум в течение трех положительных фронтов тактовой частоты.

Мы можем записать свойство как

property p;
@(posedge clk) $rose(a) -> a[*3];
endproperty

Свойство не работает в приведенном ниже случае.

clk _ _ _ | = = = | _ _ _ | = = = | _ _ _ | = = = | _ _ _ | = = = |

a _ _ | = = = | _ _ | = = = = = = = = = = = = = = = = = =

Это не соответствует спецификации, где a опускается ниже в середине, но будет подниматься вверх следующей позой, и, следовательно, приведенное выше утверждение не улавливает это.

Может ли кто-нибудь сказать, есть ли способ написать утверждение, чтобы отловить эту ошибку?

Спасибо


system-verilog system-verilog-assertions assertions
person user1978273    schedule 08.02.2015    source источник

Ответы (2)


arrow_upward
0
arrow_downward

Вы здесь что-то путаете. Записывая синхронизированное утверждение для сигнала a, вы подтверждаете, что это синхронный сигнал с определенным поведением.

Синхронные сигналы могут давать сбои между фронтами тактовых импульсов, потому что они там никогда не дискретизируются. Именно по этой причине в настоящее время мы используем синхронные сигналы, то есть для того, чтобы сигнал успел установить свое значение, прежде чем мы его дискретизируем.

Если ваш сигнал a не должен давать сбой по какой-то причине (я не дизайнер, поэтому не знаю, где это может быть полезно), насколько я знаю, вы бы узнали это с помощью какого-то инструмента для линтинга. (например, Spyglass), который выполняет структурный анализ кода HDL.

person Tudor Timi    schedule 08.02.2015

arrow_upward
0
arrow_downward

Тюдор прав, что в большинстве случаев не имеет значения, что происходит между фронтами часов. Но в CDC или асинхронном дизайне мы должны убедиться, что в дизайне нет сбоев. Есть способ сделать это наизнанку. (Я нашел это решение на http://www.verificationguild.com/modules.php?name=Forums&file=viewtopic&p=20045)

property detect_glitch;
    time leading;                  // declare the last edge occurence variable
    @(glitch)                      // At every change of glitch signal
        //The following line saves the current time and check
        // the delay from the previous edge.
        (1, leading = $time) |=> (($time - leading) >= duration);
endproperty : detect_glitch

DETECT_GLITCH : assert property (detect_glitch)
else
    $display ("ERROR");
person betontalpfa    schedule 27.10.2015