Квалификационное событие повторения непоследовательной операции SVA

У меня есть следующее свойство:

property p;
  @(posedge clk) a |=> b[=2] ##1 c;
endproperty

Он сообщает нам, что если a утвержден, то начать со следующего clk, b должен быть утвержден непоследовательно два раза, за которым следует c в любое время после последнего b.

Мой вопрос в том, что, если c заявлено между первым b и вторым b. Следует ли утверждение немедленно потерпеть неудачу или продолжить? В каком-то справочнике написано, что он должен выйти из строя, но я в этом сомневаюсь. Какое ожидаемое поведение?


system-verilog system-verilog-assertions
person AldoT    schedule 02.12.2015    source источник

Ответы (2)


arrow_upward
3
arrow_downward

[= или оператор непоследовательного повторения аналогичен goto repetition, но выражение не обязательно должно быть истинным в тактовом цикле до того, как c станет истинным .

Допустим, заявлено a. Условие импликации выполнено, и утверждение дополнительно оценивается.

После этого b проверяется два раза, независимо от того, что такое c. После того, как b будет подтверждено для двух непоследовательных фронтов тактовых импульсов, после этого c проверяется после 1-тактового цикла (из-за ##1).

Если c подтвержден и отменен, когда b проверяется дважды, то это переключение не обдуманный. Что из c считается после 2 утверждений b.

Следующие снимки дадут четкое представление:

Прохождение оснастки:

Пройдено

Неудачный щелчок:

Неудача

Здесь, несмотря на то, что в c был сбой, утверждение не прошло.

Дополнительные сведения см. В Практическом руководстве по утверждениям SystemVerilog pdf. Учебник Doulos также подойдет.

person sharvil111    schedule 02.12.2015
comment
Работает ли это также для goto repetition (я имел в виду, что когда b проверяется два раза, мы можем игнорировать c? Т.е. не удастся ли эта последовательность: a !b b c !c !b b c, если мы используем goto repetition или non-consecutive repetition? - person AldoT; 02.12.2015
comment
Не ищите c, когда проверяется b. Для упомянутой последовательности c обнаруживается после проверки b, два раза. Таким образом, ни один из двух не завершится неудачей, оба будут пройдены. Но если у вас есть что-то вроде a !b b !b b !b c, тогда goto repetition не удастся, но непоследовательное повторение пройдет. И да, это также относится к повторению goto. - person sharvil111; 02.12.2015
comment
Хорошо, теперь я понимаю и согласен с вами. Меня просто смутило утверждение в предоставленной вами ссылке: doulos.com/knowhow / sysverilog / tutorial / assertions, где в аналогичном свойстве говорится: This means a is followed by any number of clocks **where c is false**, and b is true between 1 and three times, the last time being the clock before c is true. Делают ли они здесь неправильное утверждение (требуется, чтобы c было ложным, когда проверяется b)? - person AldoT; 02.12.2015
comment
о, это вопрос интерпретации, не существует строгого условия, при котором c должен быть ложным. Просто этот c не проверяется во время моделирования. - person sharvil111; 02.12.2015

arrow_upward
0
arrow_downward

Короче да пройдет. Независимо от того, где утверждается c, после того, как будут соблюдены два «b», он будет ждать, пока c == 1. Итак, если c было 1 с самого начала и никогда не стремится к нулю, он тоже пройдет.

Еще один момент, который следует отметить, - это когда это утверждение действительно потерпит неудачу. Он пройдет, когда c будет утвержден, но если нет, он будет работать до конца теста! Вы увидите отказ только в конце моделирования.

person Convergent    schedule 03.12.2015