SystemVerilog: подразумевает оператор против |->

Question

Недавно возник вопрос, в чем разница между обычным имплицитным оператором (|->) и implies оператор в SystemVerilog. К сожалению, я не смог найти четкого ответа. Однако я собрал следующую информацию:

Из SystemVerilog LRM 1800-2012:

• § 16.12.7. Подразумевает и если свойства:

  property_expr1 implies property_expr2
  Свойство этой формы оценивается как истинное, если и только если свойство property_expr1 оценивается как ложное, или property_expr2 оценивается как истинное.

• § F.3.4.3.2 Производные логические операторы:

  p1 implies p2 ≡ (not p1 or p2)

• § F.3.4.3.4 Производные условные операторы:

  (if(b) P) ≡ (b |-> P)

Тем не менее, LRM на самом деле не указывает, какова реальная разница. Я предполагаю, что они отличаются в оценке в случае ложного антецедента (успех против пустого успеха), но я не мог найти источник или свидетельство для этого предположения. Более того, я знаю, что implies оператор очень часто встречается в сочетании с инструментами формальной проверки, такими как OneSpin.

Кто-нибудь может мне помочь?

PS: Кажется, что есть ответ на этот вопрос в следующей книге: SystemVerilog Assertions Handbook, 3rd Edition. Но 155 долларов - это слишком много для меня, просто чтобы получить ответ на этот вопрос:)

Answer 1

Я думаю, что есть даже более существенная разница. Предположим, что у нас есть следующий пример:

property p1;
  @ (posedge clk) 
  a ##1 b |-> c;
endproperty

property p2;
  @ (posedge clk) 
  a ##1 b implies c;
endproperty

assert property (p1);
assert property (p2);

Оба имплицитных оператора просто по-разному ведут себя. Имущество p1 будет запущен через матч a ##1 b и будет искать соответствие c в течение того же тика b, Однако собственность p2 вызвано a ##1 b и проверим на совпадение c во время часового цикла a, Это означает, что свойства будут соответствовать следующим сценариям:

Свойство p1 проходит, а p2 не выполняется:Свойство p2 проходит, а p1 не выполняется:

Подсказка для этого поведения может быть найдена в SystemVerilog LRM. Определенные замены:

(if(b) P) = (b |-> P)
p1 implies p2 = (not p1 or p2)

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

Answer 2

Я попробовал это и, видимо, |-> не допускается для свойств (только для последовательностей и логических выражений). Вот что я попробовал:

  property a_and_b;
    @(posedge clk)
    a && b;
  endproperty

  property a_and_c;
    @(posedge clk)
    a && c;
  endproperty

Первая форма с использованием |-> не компилируется:

// this doesn't compile
assert property(a_and_b |-> a_and_c);

Вторая форма с использованием implies компилирует:

// this does compile
assert property(a_and_b implies a_and_c);

Семантически, это так, как это для |-> оператор. когда a_and_b не получается, утверждение пусто проходит. Если a_and_b успешно, но b_and_c нет, тогда выдается ошибка.