Я хочу написать утверждение, в котором говорится, что требование должно стать высоким через 4 цикла после следующего выполнения. Для меня при перезагрузке проделанное уже высоко. Как я могу сделать запрос высоким при следующем выполнении.assert property {$rose(done) |-> ##4 req} Но я не знаю, почему он не работает. Кто-нибудь может помочь?
Системное утверждение Verilog — $rose
comment
Что значит не работает?
- person Tudor Timi schedule 05.08.2016
Ответы (1)
Если готово начинается высоко, и вы хотите подождать, пока оно упадет, а затем снова поднимется, попробуйте:
assert property (!done ##1 $rose(done) |-> ##4 req)
Но это просто гарантирует, что req будет высоким через четыре цикла после нарастающего фронта готовности. В нем ничего не говорится о том, когда это произойдет (могло быть два цикла назад, могло быть до того, как было сделано, даже подтверждено). Если вы хотите, чтобы req повышался строго через четыре цикла после выполнения, попробуйте вместо этого:
assert property (!done ##1 $rose(done) |-> ##4 $rose(req))
person
teadotjay
schedule
04.08.2016
Спасибо TJ, но любое из решений не работает. Я не могу контролировать сигнал Done, я могу только дать ссылку на этот сигнал (я не могу сделать Done низким). Добавил картинку к вопросу для пояснения. В основном он должен стать высоким после следующего нарастающего фронта.
- person eshan kanoje; 04.08.2016
@TJ
!done ##1 $rose(done) эквивалентен $rose(done) с точки зрения совпадения. (обнажая любые неизвестные значения для готово, т. е. X или Z). Просто время начала разное.
- person Tudor Timi; 05.08.2016
@TJ Если вы хотите, чтобы
req стало высоким ровно через 4 цикла после завершения, вы должны сказать: $rose(done) |-> !req [*4] ##1 req
- person Tudor Timi; 05.08.2016
@Tudor, который я обнаружил с помощью симуляторов (и некоторых инструментов FV), $rose сам по себе соответствует первому циклу ложно, потому что done изменяется с неизвестного на 1. Кроме того, я позволил req упасть, а затем снова подняться после сделанных утверждений, поэтому ваш код является более строгий.
- person teadotjay; 05.08.2016
@eshankanoje Я только что попробовал это на тестовом дизайне, и, похоже, это работает. Я обновлю свой ответ формой волны-свидетеля, как только эта часть заработает (новый инструмент FV, получение помощи от AE).
- person teadotjay; 05.08.2016
@Т.Дж. Правда, и ОП сказал, что хочет отфильтровать начальный
done при выходе из сброса.
- person Tudor Timi; 07.08.2016
@eshankanoje Может быть, вы хотите сосредоточиться на ситуации, из-за которой
done понизился, и использовать это как триггерное условие: done_goes_low_because whatever ##[*] $rose(done) ....
- person Tudor Timi; 07.08.2016
@Tudor Вот в чем моя проблема, я не могу контролировать сигнал готовности. Инструмент рандомизирует переход готового сигнала. Я могу только дать ссылку на этот сигнал.
- person eshan kanoje; 08.08.2016
@eshankanoje Правильно, инструмент FV будет играть роль чрезмерно усердного инженера по проверке и пытаться сломать ваш дизайн любым возможным способом, в том числе начать с низкого уровня, если это не нарушает протокол (который вы указываете с помощью
assume property). Таким образом, вы можете попробовать assume property($fell(reset) |-> done) сохранить высокий уровень готовности при сбросе. Имейте в виду, что любые установленные вами предположения (ограничения) должны быть проверены на следующем уровне, иначе вы можете просто маскировать потенциальную ошибку.
- person teadotjay; 09.08.2016
@TJ Точно. Я использую активный низкий сброс, поэтому также не могу использовать вышеуказанное предположение. Я придумываю что-то вроде этого. ` 1. $rose(done) |-› ##4 req 2. $fell(done) |=› !req 3. !done |-› !req`. Но все еще сталкивается с проблемами. Не могли бы вы предложить что-нибудь
- person eshan kanoje; 09.08.2016
