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

Давайте рассмотрим простой пример d-триггера с асинхронным сбросом.

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

Однако как зафиксировать поведение сброса в assertion. Я пробовал подписаться на несколько

assert @(posedge rst) (1'b1 |-> !Q);

assert @(posedge rst) (1'b1 ##0 !Q);

оба эти утверждения терпят неудачу, я думаю, потому что нет следующей постановки первого?

assert @(posedge clk) ($rose(rst) |-> !Q);

проходит, но требует свободных часов и устанавливается между двумя краями часов (не заданное поведение для первого)

 assert #0 (not (rst & Q));

Насколько я понимаю, это правильное немедленное утверждение, однако я не вижу, как это проходит / не работает в средстве просмотра сигналов. Более того, я думаю, что не смогу написать прикрытие по последнему типу утверждений.


system-verilog system-verilog-assertions assertions
person wisemonkey    schedule 12.02.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Утверждения не выполняются, потому что перед обновлением выполняется выборка Q. Выборка происходит в левой части триггерного события на ранней стадии планировщика симулятора. Q обновляется в реактивной области, которая находится позже в порядке планирования.

Легкий способ исправить это - добавить небольшую задержку, такую ​​как 1step в SystemVerilog. Я предлагаю поставить rst в условие проверки, которое может работать как часть проверки минимальной ширины импульса.

wire #(1step) rst_delay = rst;
assert @(posedge rst_delay) (1'b1 |-> rst && !Q);

Если вы моделируете с задержкой reset-to-q, например, с аннотацией SDF или искусственной задержкой, добавьте смещение к rst_delay.

wire #(r2q+1step) rst_delay = rst;
assert @(posedge rst_delay) (1'b1 |-> rst && !Q);
person Greg    schedule 13.02.2014
comment
Спасибо, обновил мое утверждение. проходят предварительные испытания. Я скрою костюм и посмотрю, что получится. Прямо сейчас мне не нужно запускать его с задержками r2q, но это полезно знать :) - person wisemonkey; 14.02.2014