Использование очередей в рекурсивных свойствах

У меня есть некоторые данные из 1-битного последовательного порта, которые кратны байтам разной длины как таковые:

byte expected_1 [$] = {8'hBA, 8'hDD, 8'hC0, 8'hDE};
byte expected_2 [$] = {8'h01, 8'h23, 8'h45, 8'h67, 8'h89, 8'hAB, 8'hCD, 8'hEF};

При каждом положительном фронте тактового сигнала отправляется один бит. Мне нужно протестировать сотни последовательностей (возможно, тысячи в будущем), поэтому я хочу автоматизировать процесс с утверждениями в системе verilog. Новый стандарт 2012 года позволяет передавать очереди свойствам, но можно ли отправлять очереди через рекурсивное свойство? Я получил некоторую ошибку об иерархической ссылке.

Это то, что у меня есть до сих пор (с помощью @Greg здесь ):

default clocking sck @(posedge sck); endclocking : sck  

sequence seq_serial(logic signal, logic [7:0] expected); // check each bit
  byte idx = 7;
  (signal == expected[idx], idx--)[*8];
endsequence : seq_serial

property recurring_queue(bit en, logic data, byte data_e [$])
  int queue_size = data_e.size;
  logic [7:0] expected = data_e.pop_front(); 

  if(queue_size != 0) (
    !en throughout (seq_serial(data, expected) ##1 recurring_queue(en, data, data_e))
  );

endproperty : recurring_queue

`define ez_assert(exp)
   assert property (recurring_queue(en, data, exp))
   else $error("Bad Sequence @ time: %t. Info: %m", $time);

Вызов утверждения в моем тестовом стенде должен быть таким простым:

A1 : `ez_assert(expected_1);

Сообщения об ошибках гласят:

1) passing hierarchical ref to be used in another hierarchical ref is not supported 
2) Illegal SVA property in RHS of'##' expression 
3) Local variable queue_size referenced in expression before getting initialized

Я открыт для других идей для утверждения длинных последовательных последовательностей переменной длины.


verification verilog system-verilog system-verilog-assertions assertions
person N8TRO    schedule 17.06.2013    source источник
comment
эти сообщения об ошибках было бы легче отслеживать, если бы они были добавлены в конец вопроса.   -  person Morgan    schedule 17.06.2013
comment
Небольшие ошибки должны быть устранены, прежде чем перейти к реальной проблеме. Присвоение всей очереди требует одинарной кавычки перед фигурной скобкой (например, q[$]='{...};). Для многострочного макроса требуется обратная косая черта ('\') в конце каждой строки, кроме последней. Ваш симулятор поддерживает передачу очереди в свойство?   -  person Greg    schedule 17.06.2013
comment
Мне нужно исправить одинарную кавычку для полного назначения очереди. Очереди, по-видимому, являются исключением, поскольку в IEEE Std 1800-2012 есть наглядные примеры. раздел 7.10 Очереди, но разрешено (10.10.3). Литералы структур (5.10), литералы массивов (5.10), неупакованные массивы (7.4), динамические массивы (7.5) и ассоциативные массивы (7.8) используют '{ для полных присваиваний.   -  person Greg    schedule 18.06.2013

Ответы (1)


arrow_upward
1
arrow_downward

Попробуйте ту же стратегию, что и seq_serial:

sequence seq_queue_pattern(bit en, logic data, byte expt_queue [$]);
    int qidx = 0;
    ( !en throughout (seq_serial(data,expt_queue[qidx]), qidx++)[*] )
    ##1 (qidx==expt_queue.size);
endsequence : seq_queue_pattern

asrt_expected_1 : assert property ( $fell(en) |-> seq_queue_pattern(en,data,expected_1));
asrt_expected_2 : assert property ( $fell(en) |-> seq_queue_pattern(en,data,expected_2));

Это утверждение не будет выполнено, если значение en высокое или цепочка seq_serial не соответствует ожидаемой. Не имеет значения расположение скобок:

  • en is don't care one clock after final seq_serial completes:
    • ( !en throughout (seq_serial(data,expt_queue[qidx]), qidx++)[*] ) ##1 (qidx==expt_queue.size)
  • en must be low one clock after final seq_serial completes or failes and don't care after that
    • !en throughout ( (seq_serial(data,expt_queue[qidx]), qidx++)[*] ##1 (qidx==expt_queue.size) )
  • en must be low one clock after final seq_serial completes and don't care after that
    • !en throughout ( (seq_serial(data,expt_queue[qidx]), qidx++)[*] ##1 (qidx==expt_queue.size) ) ##1 (qidx==expt_queue.size)

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

`define asrt_qpat(en,monitor, expt_queue) \
    sequence seq_queue_pattern__``expt_queue (bit en, logic data); \
        int qidx = 0; \
        (!en throughout (seq_serial(data,expt_queue[qidx]), qidx++)[*]) \
        ##1 (qidx==expt_queue.size); \
    endsequence : seq_queue_pattern__``expt_queue \
    \
    asrt_``expt_queue : assert property( @(posedge clk) \
        $fell(en) |=> seq_queue_pattern__``expt_queue (en,monitor) ) \
    else $error("Bad Sequence @ time: %t. Info: %m", $time);

`asrt_qpat(en,data[0],expected_1)
`asrt_qpat(en,data[1],expected_2)
person Greg    schedule 17.06.2013
comment
У меня он запущен и работает, но по другому маршруту. В итоге мне пришлось использовать fork-join и указать ожидаемое количество байтов. (Кое-что о неограниченном диапазоне) Я попробую ваш метод, когда у меня будет шанс. Спасибо за отличные ответы. - person N8TRO; 18.06.2013
comment
Мне любопытно посмотреть на ваш подход. Чем помогает fork-join? - person Greg; 18.06.2013
comment
Fork-join не помог. Ваш код почти работает, но это смещение в 1 байт (assert проверяет 1 байт позже) - person N8TRO; 18.06.2013
comment
Ты имеешь в виду немного опоздал? Измените |=> на |->, если это так. - person Greg; 18.06.2013
comment
Извините, утверждение начинается в правильное время, но завершается ошибкой на 1 байт позже. Может ли это быть (seq_ser(..),qidx++)[*] ##1 (qidx==expt_queue.size) В сообщении говорится, что qidx = 0 во время ошибки. Я никогда не видел [*] сам по себе.. Как это работает? - person N8TRO; 18.06.2013
comment
[*] — это сокращение от [*0:$] (от нуля до бесконечности) Стандарт IEEE 1800-2012< /а> 16.9.2. Это может быть ваш тестовый вектор. Вы ставите пробелы между байтами? Я использую en<=1;fork ##1 cb.en<=0; foreach(expected_1[i,j]) ##1 cb.data[0]<=expected_1[i][j]; foreach(expected_2[i,j]) ##1 cb.data[1] <= expected_2[i][j]; join Можете ли вы поделиться своим кодом тестового стенда или предоставить сигнал? - person Greg; 18.06.2013
comment
давайте продолжим это обсуждение в чате - person N8TRO; 18.06.2013