Утверждения SystemVerilog: После подтверждения A, A остается высоким, пока B не будет отменено, и после этого A, наконец, будет низким

Question

Я пытался написать утверждение:

Как только A подтвержден, A остается ВЫСОКИМ, пока B не будет отменен. После этого А окончательно откажется.

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

my_assertion : assert property(
    @(posedge clk) disable iff(reset)
    $rose(A) |-> A throughout !B [->1] ## [0:$] !A) 
else $display("Assertion failed") 

Утверждение не выполнено в тот момент, когда A отменяется. Ребята, подскажите пожалуйста, где я ошибся в my_assertion? "[0: $]" был использован неправильно?

Answer 1

Я думаю, что ваша проблема связана с приоритетом оператора. Это не дает сбоя, когда A сброшен:

$rose(A) |-> (A throughout !B [->1]) ## [0:$] !A

тогда как то, что вы написали, совпадает с:

$rose(A) |-> A throughout (!B [->1] ## [0:$] !A)

, который никогда не пройдет, потому что A не может быть истинным и ложным одновременно.

https://www.edaplayground.com/x/4Vv9

Answer 2

## имеет более высокий приоритет, чем throughout;См. IEEE1800-2012 § 16,9 Операции с последовательностями Таблица 16-1.

Поэтому A throughout !B [->1] ## [0:$] !A является выборкой a A throughout (!B [->1] ## [0:$] !A).Это терпит неудачу, потому что A требуется быть высоким (левая сторона throughout) и низким (правая сторона throughout) для последнего цикла, который всегда будет оцениваться как ложный.

Я считаю желаемоеповедение: (A throughout !B [->1]) ## [0:$] !A