SVA - Есть ли способ проверить шаблон переменной переменной в последовательном выводе переменной длины с использованием утверждения системного Verilog?

Например, у меня есть шаблон pt = 1101, который нужно проверить на последовательном выходе s_out = 1011101110111011 (сначала младший бит). Я пытаюсь проверить «pt» в «s_out» только с помощью SVA без использования блока always. Примечание: pt и s_out имеют переменную длину.

Я пытаюсь использовать два счетчика для длин pt и s_out, но не знаю, как их использовать в SVA.

Любые предложения будут очень полезны. Спасибо, Сусун


system-verilog system-verilog-assertions
person susun    schedule 12.08.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Вы можете объявлять внутренние переменные в последовательностях и в свойствах. У них также могут быть входные аргументы. Вот как я подхожу к вашей проблеме:

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

sequence pattern_in_output(pattern, int unsigned len);
  int unsigned count = 0;
  (
    s_out == pattern[count],
    $display("time = ", $time, " count = ", count),
    count += 1
  ) [*len];
endsequence

Обратите внимание, что аргумент pattern не типизирован. Я также оставил там несколько отладочных отпечатков, чтобы вы могли посмотреть, как это работает. Как только эта последовательность начинается, она проверяет len циклов, s_out совпадающих с соответствующим битом pattern.

Я не знаю, каковы ваши точные условия для проверки (когда именно вы хотите начать и остановиться), поэтому я просто предположил, что у вас есть сигнал с именем tx, который сообщает вам, передаете ли вы в данный момент или нет (1 означает, что вы передаете, поэтому мы нужно проверить, 0 означает, что нет, следовательно, нет проверки).

Свойство будет выглядеть примерно так:

assert property (
  @(posedge clk)

  // check first group
  $rose(tx) |-> pattern_in_output(pt, 4)

  // if 'tx' is still high, need to check for another occurence
  // - repeat this forever
  ##1 tx |-> pattern_in_output(pt, 4)

  // this line causes and internal error
  //##1 tx |-> pattern_in_output(pt, 4) [+] or !tx

  // this prints when the property exits
  ##0 (1, $display("exited at ", $time))
);

Начинаем проверку по нарастающему фронту tx. Ищем совпадение с нашей ранее определенной последовательностью. Впоследствии может случиться так, что мы все еще передаем, и нам нужно проверить второе вхождение шаблона. Если после этого второго появления tx по-прежнему 1, нам нужно проверить наличие третьего и так далее.

Здесь я должен извиниться за то, что оставил вам половину ответа. Я делал этот пример на EDAPlayground и не мог заставить его работать (я продолжал получать внутренние ошибки симулятора). Строка ##1 tx |-> pattern_in_output(pt, 4) проверяет только второе появление. Тот, что под этим (закомментирован), ##1 tx |-> pattern_in_output(pt, 4) [+] or !tx, должен проверять любое последующее вхождение шаблона, пока tx все еще 1, и прекращать сопоставление, как только оно становится 0.

Вам придется самостоятельно повозиться с деталями, но я думаю, на ваш вопрос был дан ответ. Вы можете увидеть, как можно использовать внутренние переменные внутри конструкций утверждения.

P.S. Если хотите, полный код (включая средства тестирования) находится здесь: http://www.edaplayground.com/x/4my

person Tudor Timi    schedule 16.09.2014