Динамическая длина параллельной последовательности утверждений SystemVerilog

У меня есть массив длины x. Выходными сигналами для данного тестового стенда будет каждое значение в массиве в соответствующем порядке от 0: x-1.

В частности, в моей проблеме массив - это коэффициенты фильтра, а тестовая среда - это импульсная характеристика. Тест должен быть самоконтролируемым, для чего потребуется последовательность с динамической длиной, так как коэффициенты будут меняться от теста к тесту.

Последовательность, которую я хотел бы, должна выглядеть примерно так:

always @(posedge clk) begin
  assert_sequence : assert property (    
        (data_out == array_1[0])
    |=> (data_out == array_1[1])
    |=> (data_out == array_1[2]) 
    |=> (data_out == array_1[3]) 
    |=> (data_out == array_1[4]) 
    |=> (data_out == 0) ) 
      $info("Seen the sequence");
    else
      $error("Sequence was incorrect");  
  end

Можно ли это делать динамически? Я пробовал использовать цикл genvar for, но он выдает ошибки. Я искал на форумах и не нашел ничего, что соответствовало бы моим требованиям.

Возможно, что-то подобное могло дать правильный ответ?

    always @(posedge clk) begin
  assert_sequence : assert property (    
        (data_out == array1[0][0])

  for(genvar i = 1; i < 5, i++) begin
    |=> (data_out == array1[i])
  end

    |=> (data_out == 0) ) 
      $info("Seen the sequence");
    else
      $error("Sequence was incorrect");  
  end

verification verilog system-verilog system-verilog-assertions synopsys-vcs
person Daniel    schedule 21.05.2020    source источник
comment
Очень интересная проблема. SVA не был бы моим первым выбором для проверки. И, кстати, шлейфовое соединение операторов импликации (|=>), вероятно, не означает то, что вы думаете. Вероятно, он не отвечает на этот вопрос, но, тем не менее, я думаю, вам следует использовать простой ##1, т.е. assert_sequence : assert property ( <some_trigger> |=> (data_out == array_1[0]) ##1 (data_out == array_1[1]) ##1 (data_out == array_1[2]) ...   -  person Matthew Taylor    schedule 21.05.2020
comment
Я не могу (с головы до ног) придумать, как бы вы поместили цикл в утверждение SVA. У вас может быть мегаутверждение, которое проверяет каждую выборку вашего импульсного отклика индивидуально и ИЛИ каждого из них с каким-то массивом масок, например ... ##1 (data_out == array_1[3]) || mask[3] ##1 ..., и вы бы сделали все дополнительные элементы массива масок (которые не требуются для более короткого импульса ответ) 1 (т.е. ИСТИНА). Но я бы подумал, что выпишу эту проверку в SystemVerilog, а не в SVA.   -  person Matthew Taylor    schedule 21.05.2020

Ответы (2)


arrow_upward
1
arrow_downward

Как уже говорилось, SVA, вероятно, здесь не естественный выбор. Однако действительно интересная проблема, поэтому пришлось немного подумать:

Вы пробовали использовать рекурсивные свойства? Что-то вроде:

property check_sequence(coefficients);
  (data_out == coefficients[0]) ##0
    ((coefficients.size() == 1) or 
     (##1 check_sequence(coefficients[1:coefficient.size()]));
endproperty

assert_label: check_sequence(array_1);

по-прежнему нужен триггер - не указанный в исходном q.

Другое дело, будет ли это наиболее эффективное или удобочитаемое решение.

person Svetlomir Hristozkov    schedule 22.05.2020

arrow_upward
0
arrow_downward

Комментарии очень полезны и содержат заметки о направлении, которое я выбрал для решения этой проблемы. Просто вернулся к проблеме и придумал это не элегантное решение.

for(genvar i = 1; i < 5; i++) begin
  always @(posedge clk) begin
    assert_sequence : assert property (
                                       (data_out == array1[0])
                               |-> ##i (data_out == array1[i])
                               |-> ##(5-i) (data_out == 0) //This line prevents error 
                                                                  //as my coefficients are symmetric
                                    )
      $info("Impulse response Coefficient %0d seen", i);
  else
      $error("Impulse response Coefficient %0d not seen", i);
  end
end

Этот код создает несколько утверждений и описывает, что, когда я вижу первый коэффициент, в i тактовых циклах я ожидаю увидеть коэффициент (i + 1), а из-за симметрии моих проблем в (5-i) тактовых циклах я увижу а 0.

person Daniel    schedule 21.05.2020