когда оцениваются значения отключения утверждений iff?

Для этого кода я вижу, что оба утверждения терпят неудачу. Кажется, что отключить iff (значение) вычисляется позже, чем само выражение. Может кто-нибудь объяснить это.

module tb();
reg clk = 1;
always #5 clk = !clk;
reg rst = 1;
always @ (posedge clk)
    rst <= 0;

initial #11ns $finish();

assert property (@ (posedge clk) disable iff (rst) 1 |-> 0);
assert property (@ (posedge clk) rst |-> 0);
endmodule

Продолжение, как бы это проверить:

always_ff @ (posedge clk or posedge rst) begin
    if (rst) q <= 0;
    else q <= d;
end

где rst сбрасывается из-за задержки:

always_ff @ (posedge clk)
    rst <= rst_a;

Похоже, что отключить iff больше не получится. как он оценивает сначала поздно.


system-verilog system-verilog-assertions
person nachum    schedule 18.04.2018    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Выражение внутри disable iff (expr) является асинхронным и использует значения без выборки. Свойство оценивается как часть наблюдаемой области, которая следует за областью NBA.

Для первого утверждения rst уже является низким ко времени первой попытки оценить свойство в момент времени 10 в наблюдаемой области. Таким образом, disable iff не препятствует попытке оценить свойство, которая всегда терпит неудачу.

Для второго свойства выборочное значение rst по-прежнему равно 1 во время первой попытки оценить свойство, поэтому оно также должно завершиться ошибкой.

Следовать за,

Я думаю, вы можете беспокоиться о непрактичном случае. Насколько вероятно, что антецедент будет верным после сброса? А если бы это было правдой, то и утверждение должно было бы оставаться в силе. Например, предположим, что у вас есть счетчик с утверждением для проверки того, что он переворачивается при достижении максимального значения.

assert property (@ (posedge clk) disable iff (rst) (counter==maxval) |=> (counter ==0) );

Если бы значение сброса счетчика было максимальным, вы бы не хотели отключать утверждение.

person dave_59    schedule 18.04.2018
comment
Не могли бы вы указать мне на часть стандарта, в которой говорится, что отключение iff (expr) оценивается в наблюдаемое время. - person nachum; 18.04.2018
comment
Я этого не говорил. См. стр. 423 LRM за 1800-2017 гг. В основном выражение оценивается включительно между начальной и конечной попытками свойства с использованием значений без выборки. Это асинхронно между попытками запуска и завершения. Но ваше свойство представляет собой один тактовый цикл, поэтому все, что имеет значение, это то, что rst уже равно 0 к моменту первой попытки оценить свойство в наблюдаемой области. - person dave_59; 18.04.2018
comment
Таким образом, отключенный iff оценивает непрерывно и начинает с наблюдаемой области одних и тех же часов. в этом есть смысл. Можете ли вы тогда объяснить, как можно отключить свойство, когда reset отменяется без задержки с использованием неблокирующего присваивания? Добавил код в вопрос. - person nachum; 19.04.2018
comment
Как насчет простейшего случая тестирования d-триггера? Я хочу убедиться, что q равно d через один час, за исключением случая сброса. В моем случае я писал код для ворот с часами (чтобы намочить ноги). - person nachum; 19.04.2018
comment
Переместите смену сброса подальше от часов posege, как на negege. Это хорошая практика для всех ваших стимулов. - person dave_59; 19.04.2018
comment
Я чувствую, что мы ходим по кругу. Спасибо за ответы. Это проясняет кучу вещей. - person nachum; 19.04.2018