Утверждение, чтобы проверить сбой в сигнале

Question

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

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

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

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

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

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

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

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

Спасибо

Answer 1

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

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

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

Answer 2

Тюдор правый, что в большинстве случаев не имеет значения, что происходит между краями часов. Но при 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");