Если последовательность встречается, то внутри нее возникает последовательность в утверждениях System-Verilog

Question

Если последовательность встречается, то внутри нее возникает последовательность в утверждениях System-Verilog

Я хочу сказать: "Если последовательность A происходит тогда последовательность B происходит в этой последовательности ". Как я могу это сделать?

Я бы подумал, что мог бы использовать утверждение:

assert property (@(posedge clk) (A |-> (B within A));

но это не похоже на мой пример.

Я прочитал это:

Говорят, что линейная последовательность совпадает по конечному интервалу последовательных тактовых импульсов, при условии, что первое логическое выражение оценивается как истинное на первом тактовом такте, второе логическое выражение оценивается как истинное на втором тактовом такте и т. Д., Вплоть до последнее логическое выражение, оцениваемое в true на последнем такте.

но я подозреваю, что тиканье часов перешло на другую сторону |-> последний тик, когда я хочу, чтобы он был первым.

Мой конкретный пример - это аккумулятор, который я ожидаю переполнить, если добавлю достаточно положительных чисел, поэтому я хочу A = (input == 1)[*MAX_SIZE] а также B = (output == 0), так вот B это последовательность длины 1, я не знаю, вызывает ли это проблемы.

Я очень новичок в system-verilog, так что, может быть, это какая-то другая часть моего кода, которая работает неправильно, но я нигде не видел, чтобы этот пример был сделан.

1

system-verilog system-verilog-assertions

Источник

user6155033 09 дек '16 в 16:30

1 ответ

Решение

Другие вопросы по тегам system-verilog system-verilog-assertions

user1334062 09 дек '16 в 19:23 2016-12-09 19:23 · Accepted Answer · 2016-12-09 19:23

Вы правы, что следствие в |-> оператор запускается один раз A уже соответствует. То, что вы хотите, это посмотреть в прошлое: "Однажды я видел Aя видел B within A?".

Вы могли бы использовать triggered Свойство последовательности, чтобы сделать это:

sequence b_within_a;
  @(posedge clk)
    B within A;
endsequence

assert property (@(posedge clk) A |-> b_within_a.triggered);

b_within_a последовательность будет точно соответствовать в конце A, конечно, если B также произошло, когда triggered свойство будет оцениваться в 1,

Обратите внимание, что b_within_a последовательность имеет свои часы, определенные специально. Это требование от LRM, в противном случае вам не разрешат звонить triggered в теме.