когда использовать системную задачу $rose с сигналом в утверждениях

Я пытаюсь понять, когда использовать $rose для сигнала в утверждении. Например, каким образом два приведенных ниже утверждения будут вести себя по-разному?

first:assert property 
        (@(posedge clk) $rose(reset) |-> (data == 0));

second: assert property
          (@(posedge clk) reset |-> (data==0));

это $rose должно использоваться с асинхронными сигналами?


person Gautam    schedule 03.09.2014    source источник


Ответы (2)


$rose означает, что в предыдущем такте сигнал был «0», а в текущем такте — «1».

Первое утверждение будет проверять только в первом цикле, когда reset становится высоким, тогда как второе утверждение будет проверять, что data равно «0» в каждом такте, когда reset высокое.

Вот хороший рисунок, показывающий, когда срабатывает каждое из утверждений.

         _   _   _   _   _   _
clk    _| |_| |_| |_| |_| |_| |_
             ___________
reset  _____|           |_______

first           x   

second          x   x   x

$rose имеет значение для синхронных сигналов.

person Tudor Timi    schedule 03.09.2014

$rose(reset) работает при переходе от 0/x/z к 1 и возвращает true при таком переходе.

reset без $rose не учитывает переход 0/x/z в 1 и возвращает false при наличии такого перехода. Это правильно?

person Abijith Prakash    schedule 09.10.2019