SVA: Использование импликации (|=›) вместо последовательности?

Свойства утверждения SystemVerilog могут быть созданы с помощью операторов импликации |=> и последовательностей ##1.

Например :

property P1;
  @(posedge clk)
    A ##1 B |=> C ##1 D;
endproperty

Выше мы использовали A ##1 B в качестве разрешающей последовательности (антецедент) и C ##1 D в качестве исполняющей последовательности (консеквент).

Я не понимаю, почему это нельзя было переписать как:

property P2;
  @(posedge clk)
    A ##1 B ##1 C ##1 D;
endproperty

Когда и почему вы предпочли бы импликацию |=> последовательности ##1?


verification system-verilog system-verilog-assertions assertions
person Morgan    schedule 20.05.2013    source источник
comment
Это не Verilog — какой здесь этикет для изменения тегов вопросов?   -  person EML    schedule 21.05.2013
comment
Я думаю, что большинство людей просто отредактируют вопрос и оставят четкое «резюме редактирования». Также не уверен, насколько мы различаем verilog и SystemVerilog в наши дни, поскольку LRM были объединены в один.   -  person Morgan    schedule 21.05.2013

Ответы (1)


arrow_upward
1
arrow_downward

Вышеупомянутые свойства одинаковы для передачи последовательности, однако условия отказа не совпадают.

Если все они равны 1, то A ##1 B ##1 C ##1 D; и A ##1 B |=> C ##1 D; верны.

Если у нас есть A как 1, то остальные 0:

A ##1 B ##1 C ##1 D; терпит неудачу, и A ##1 B |=> C ##1 D; проходит.

Последнее не считается отказом из-за несоблюдения условий разрешающей последовательности.

person Morgan    schedule 20.05.2013