В чем разница между импликацией (- ›) и ## 0 в SVA?

Первое, что вам нужно проверить, это синтаксис единственного оператора импликации a |-> b.

В утверждении SystemVerilog есть два выражения.

1. a ##0 b
2. a |-> b

Собственно, по выражениям это похоже. Сначала в этом выражении проверяется, что a утверждается (1), а после 0 такта b утверждается (1) или нет. Второе выражение проверяет, что b (включен) утверждается, когда утверждается a (1), затем на той же позиции b утверждается (1) или нет.

На практике, когда инженеры по верификации писали такие утверждения, они заботятся о следующих вещах.

1. a ##0 b: В этом выражении, если a не утвержден, это означает сбой.

Когда a утверждается (1) и на той же отметке времени b не утверждается, то также отображается сбой.

2. a |-> b: В этом выражении, если заявлено a, а не утверждено b, будет отображаться ошибка.

Если a не подтвержден, то он не будет проверять, подтверждено ли b. Это поведение отличается от a ##0 b.

Если вы примените разные входные данные, вы увидите, что выражение a ##0 b даст вам больше ошибок, чем a |-> b. Причина того же уже объяснена выше.

Еще одна вещь, на которую следует обратить внимание: «Конструкция импликации может использоваться только с определениями свойств. Она не может использоваться в последовательностях».

Спасибо,

Ашутош

Ваш вопрос иллюстрирует важность оператора импликации (|->). В этом примере используется оператор импликации, и он полезен:

a -> b означает «если a истинно, то b должно быть true» (полезно).

Это не очень полезно и обычно не очень полезно:

a ##0 b означает, что «a и b оба должны быть верными всегда» (не очень полезно).

https://www.edaplayground.com/x/47iN