Я не смог найти значение выражения [->]. Я знаком с использованием диапазонов как [a:b] или таких последовательностей, как EVENT1|->EVENT2, но не с той, которую я упомянул в начале.Значение [-> 1] в определении свойства системы verilog
Контекст - это свойство assert, которое гарантирует, что clk1 всегда переключается при низком сбросе.
@(clk2) disable iff(rst) !$stable(clk1)[->1];
Идея на что [->] на самом деле означает?
Заранее благодарен!
[->N] означает «неповторимое точное повторение». a[->N] означает N не последовательных повторений a, причем совпадение происходит именно после N-го повторения a.
Так, например, a ##1 b[->2] ##1 c будет соответствовать
_
a _______/ \_____________________
| _ _
b _________________/ \___/ \_____
| _
c _________________________/ \___
| |
| |
match |<----------------->|
но не
_
a _______/ \___________________________
_ _
b _________________/ \___/ \___________
_
c _______________________________/ \___
[=N] означает "непоследовательное повторение". a[=N] означает N последовательных повторений a, причем совпадение происходит в любое время после N-го повторения a.
Так, например, a ##1 b[=2] ##1 c будет соответствовать второму рисунку, выше.
Я верю точно так же. Но можете ли вы сказать, что неудачный шаблон '[= N]' не будет выполнен. Я видел, что подобные утверждения повторяются во время моделирования, когда 'c' не приходит, но никогда не терпит неудачу. – sharvil111
@ sharvil111 Вопрос в 64 000 $ ... если 'a ## 1 b [= 2] ## 1 c' является _condition_, а не _precondition_, и нет предела времени, когда c должен прибыть, тогда это утверждение никогда не будет потерпеть неудачу. Если есть время, когда c должен прибыть, то требуется некоторая модификация. –
Спасибо за объяснение @Mathew Taylor. Материал предпосылки делает это в значительной степени ясным. Я думаю, что 'a ## 1 [= 2] b ## 1 c' и' a ## 1 b [= 2] ## [1: 3] c' - одно и то же. Поскольку для 'c' не существует границы. Пожалуйста, поправьте меня, если я ошибаюсь. – sharvil111
Есть в основном 3 оператора, как это:
Последовательная Повторения [* п] -
(a ##1 b[*2] ##1 c) = (a ##1 b ##1 b ##1 c)
Это означает, что этого, следует утверждать, после того, что б должны быть заявлены на подряд 2 тактику часов, следуя утверждению c в следующем такте.
Гото Повторение [-> п] -
(a ##1 b[->2] ##1 c) = (a ##1 ((!b[*0:$] ##1 b)[*2]) ##1 c)
Это означает, что, A следует утверждать, что после того, как б должны быть заявлены на 2 тиков часов, но не последовательно. И как только б утверждается 2 часов клещами, на следующем такте с должны получить утверждал
непоследовательных Повторения [= п] -
(a ##1 b[=2] ##1 c) = (a ##1 ((!b[*0:$] ##1 b)[*2]) ##1 !b[*0:$] ##1 c)
Это означает, что этого, следует утверждать, после этого b следует утверждать на 2 тактовых сигналах, но не последовательно. И как только b утверждается на 2 такта, c должен получить подтверждение, прежде чем b снова получит 3-й раз.
Помните, что разница между [-> п] оператора & [= п], связано с последний операнд "с". В [-> 2] с следует утверждать, что на следующем часе отметьте галочкой, как только b будет указано дважды (не последовательно).Но в [= 2], с должны быть заявлены до б получает утверждал, 3-й раз (не последовательно)
Есть в основном операторы 3 повторения, доступные в системе Verilog, как указано и описано в других ответах.
Код
@(clk2) disable iff(rst) !$stable(clk1)[->1];
можно интерпретировать следующим образом:
'Отключить' свойство утверждение, если 'первый' является высокой. Если это не так, проверьте, нет ли «clk1» нестабильно для изменений «1» clk2 (от высокого к низкому или от низкого до высокого), не обязательно при последовательных изменениях часов clk2.
, что означает, что утверждение:
не получит инвалида (т.е. ни пройти, ни терпеть неудачу), если первый равен 1.
будет проходить, если CLK1 не является стабильным (остается в состояние, т.е. высокое или низкое) для изменения 1 clk2. Но не обязательно, чтобы clk1 был неустойчив при последовательных изменениях часов clk2.
проиграет иначе.
Это указывает на то, что вы хотите проверить, работает ли clk1 на более высокой частоте, чем clk2.
Разве это не _System_-Verilog, а не Verilog? –