Значение [-> ​​1] в определении свойства verilog системы

Question

Я не смог найти значение [->] выражение. Я знаком с использованием диапазонов как [a:b] или последовательности, такие как EVENT1|->EVENT2Но не с тем, что я упоминал в начале.

Контекст является свойством assert, которое гарантирует, что clk1 всегда переключается при низком уровне сброса.

@(clk2) disable iff(rst) !$stable(clk1)[->1];

Любая идея о том, что [->] действительно значит?

Заранее спасибо!

Answer 1

Есть в основном 3 таких оператора:

Последовательное повторение [* n] -

(a ##1 b[*2] ##1 c) = (a ##1 b ##1 b ##1 c)

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

Перейти к повторению [-> n] -

(a ##1 b[->2] ##1 c) = (a ##1 ((!b[*0:$] ##1 b)[*2]) ##1 c)

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

Непоследовательное повторение [= n] -

(a ##1 b[=2] ##1 c) = (a ##1 ((!b[*0:$] ##1 b)[*2]) ##1 !b[*0:$] ##1 c)

Это означает, что a следует утверждать, после этого b следует устанавливать на 2 тактах, но не последовательно. И как только b заявлено на 2 тактах, c должно быть подтверждено, прежде чем b снова будет подтверждено в 3-й раз.

Помните, разница между оператором [->n] & [=n] связана с последним операндом "c". В [->2], c должен быть установлен на следующем такте, как только b будет введен дважды (не последовательно). Но в [=2] должно быть указано c, прежде чем b будет подтверждено в 3-й раз (не последовательно)

Answer 2

[->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 будет соответствовать второму шаблону выше.

Answer 3

Как правило, в системном verilog доступно 3 оператора повторения, как указано и объяснено в других ответах.

Код

    @(clk2) disable iff(rst) !$stable(clk1)[->1];

можно интерпретировать следующим образом:

"Отключить" свойство утверждения, если значение "rst" высокое. Если это не так, проверьте, является ли "clk1" нестабильным для "1" изменений тактового сигнала clk2 (с высокого на низкий или с низкого на высокий), необязательно при последовательных изменениях тактового сигнала clk2.

что означает, что утверждение:

• будет отключен (то есть ни пройден, ни не пройден), если первое равно 1.

• будет проходить, если clk1 нестабилен (остается в том состоянии, в котором он находится, то есть либо на высоком, либо на низком уровне) в течение 1 смены часов clk2 Но необязательно, что clk1 должен быть нестабильным при последовательных изменениях часов clk2.

• иначе не получится.

Это говорит о том, что вы хотите проверить, работает ли clk1 на более высокой частоте, чем clk2.