В чем разница между символом «-›» и «|-›» в свойствах утверждения System Verilog

Я столкнулся с примером свойства, которое работает здесь:

property p_a;
    @(posedge clk) $rose(a) -> $rose(b);
endproperty

Синтаксической ошибки выше нет.

Затем я попытался изменить это

property p_a;
    @(posedge clk) $rose(a) -> ##2 $rose(b);
endproperty

Что дает мне синтаксическую ошибку, только чтобы понять, что на самом деле это не '|->'

property p_a;
    @(posedge clk) $rose(a) |-> ##2 $rose(b);
endproperty

Это работает, так что же на самом деле представляет собой символ -> в свойстве? Я знаю, что обычно это вызывает событие.


implication system-verilog-assertions
person シアジョナサン    schedule 03.12.2020    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Оператор -> является оператором логического следствия, работает с логическими операндами:

Логическое следствие выражение1 –›выражение2 логически эквивалентно (!выражение1 || выражение2)

|-> — это последовательная импликация, используемая для выражения определенных временных свойств.

Конструкция импликации указывает, что проверка свойства выполняется условно при совпадении с последовательным антецедентом... Эта конструкция используется для предусловного мониторинга выражения свойства и разрешена на уровне свойства. Результат импликации либо истинен, либо ложен. Левый операнд sequence_expr называется антецедентом, а правый операнд property_expr называется консеквентом...

Другими словами, первый можно использовать для логических функций, второй — для последовательностей событий. Они очень разные.

person Serge    schedule 04.12.2020