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

Question

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

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

Однако как зафиксировать поведение сброса в утверждении. Я попытался следующие несколько

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

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

обе эти утверждения не получится, я думаю, потому что нет рядом posedge из RST?

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

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

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

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

Answer 1

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

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

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

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

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