Избегайте кода поддержки для последовательности SVA для обработки конвейерной транзакции

Question

Предположим, у нас есть протокол, в котором говорится следующее. После того, как мастер устанавливает req к fill, ведомый сигнал 4 передачи с помощью rsp:

Последовательность СВА для всей этой операции будет (при условии, что ведомый может вставить idle циклов между trans циклов):

req == fill ##1 (trans [->1]) [*4]; 

Теперь предположим, что хозяину разрешено запрашивать конвейер. Это означало бы, что следующий fill разрешено начинать до того, как 4 trans циклы выполняются:

Последовательность SVA сверху не поможет, потому что для второго fill это будет неправильно соответствовать 4 trans циклов, оставив последний trans «плавающий». Необходимо было бы начать сопоставление trans циклов только после того, как совпадают предыдущие fill.

Последовательность требует глобальной информации, недоступной в рамках одной оценки. В основном, он должен знать, что другой экземпляр его запущен. Единственный способ, которым я могу думать о реализации этого использует некоторый RTL код поддержки:

int num_trans_seen; 
bit trans_ongoing; 
bit trans_done; 
bit trans_queued; 

always @(posedge clk or negedge rst_n) 
    if (!rst_n) begin 
    num_trans_seen; 
    trans_ongoing <= 0; 
    trans_done <= 0; 
    trans_queued <= 0; 
    end 
    else begin 
    if (trans_ongoing) 
     if (num_trans_seen == 3 && req == trans) begin 
     trans_done <= 1; 
     if (req == fill || trans_queued) 
      trans_queued <= 0; 
     else 
      trans_ongoing <= 0; 
     num_trans_seen == 0; 
     end 
    else 
     if (trans_queued) begin 
     trans_queued <= 0; 
     trans_ongoing <= 1; 
     end 

    if (trans_done) 
     trans_done <= 0; 
    end 

выше код должен поднять trans_ongoing немного, пока транзакция продолжается и пульс trans_done в такте, когда последний trans для fill отправлено. (. Я говорю должно, потому что я не проверял, но это не точка Давайте предположим, что он работает.)

Имея что-то вроде этого, можно было бы переписать последовательность быть:

req == fill ##0 (trans_ongoing ##0 trans_done [->1]) [*0:1] 
    ##1 (trans [->1]) [*4]; 

Это должно сработать, но я не особо волнуюсь о том, что мне нужен код поддержки. В нем много избыточности, потому что я в основном переработал хороший кусок того, что такое транзакция и как работает конвейерная обработка. Это также не так легко повторно использовать. A sequence можно поместить в пакет и импортировать в другое место. Код поддержки может быть помещен только в некоторый модуль и повторно использован, но это другой логический объект, чем пакет, который сохранит последовательность.

Вопрос здесь: есть ли способ написать конвейерную версию последовательности, избегая при этом необходимости поддержки кода?

Answer 1

Похоже, что rsp всегда простаивает до начала транс. Если RSP-х idle является постоянной величиной, и это значение, которое trans никогда не будет, то вы можете использовать:

req == fill ##0 (rsp==idle)[->1] ##1 trans[*4]; 

выше должен работать, когда трубопровод поддерживает 1 до 3 этапов.

Для трубопровода глубиной 4+, я думаю, вам нужен вспомогательный код. Блоки успеха/отказа утверждения могут быть использованы для некомпетентности подсчета завершенных trans; это избавит вас от записи дополнительного RTL. Локальная переменная в свойстве может использоваться для выборки значения счета заполнения. Выбранное значение будет использоваться в качестве критерия для начала выборки ожидаемого шаблона переноса.

int fill_req; 
int trans_rsp; 
always @(posedge clk, negedge rst_n) begin 
    if(!rst_n) begin 
    fill_req <= '0; 
    trans_rsp <= '0; 
    end 
    else begin 
    if(req == fill) begin 
     fill_req <= fill_req + 1; // Non-blocking to prevent risk of race condition 
    end 
    end 
end 

property fill_trans(); 
    int id; 
    @(posedge clk) disable iff(!rst_n) 
    (req == fill, id = fill_req) |-> (rsp==idle && id==trans_rsp)[->1] ##1 trans[*4]; 
endproperty 

assert property (fill_trans()) begin 
    // SUCCESS 
    trans_rsp <= trans_rsp + 1; // Non-blocking to prevent risk of race condition 
end 
else begin 
    // FAIL 
    // trans_rsp <= trans_rsp + 1; // Optional for supporting pass after fail 
    $error("..."); 
end 

FYI: У меня не было времени полностью проверить это. Это должно по крайней мере привести вас в правильном направлении.

---

---

Я экспериментировал немного больше и нашли решение, которое может быть более по своему вкусу; нет кода поддержки.

Эквивалент trans[->4] является (!trans[*] ##1 trans)[*4] за IEEE Std 1800-2012 § 16.9.2 Повторение в последовательности. Поэтому мы можем использовать локальные переменные для обнаружения новых запросов на заполнение с расширенной формой. Например, следующая последовательность

sequence fill_trans; 
    int cnt;        // local variable 
    @(posedge clk) 
    (req==FILL,cnt=4) ##1 (    // initial request set to 4 
    (rsp!=TRANS,cnt+=4*(req==FILL))[*] // add 4 if new request 
    ##1 (rsp==TRANS,cnt+=4*(req==FILL)-1) // add 4 if new request, always minus 1 
)[*] ##1 (cnt==0);      // sequence ends when cnt is zero 
endsequence 

Если нет другого классификатор не упоминается, вы не можете использовать типичный assert property();, потому что он начнет новое утверждение темы с каждый раз, когда есть запрос заливки. Вместо этого используйте инструкцию expect, которая позволяет ждать оценки имущества (IEEE Std 1800-2012 § 16.17 Expect statement).

always @(posedge clk) begin 
    if(req==FILL) begin 
    expect(fill_trans); 
    end 
end 

Я попытался воссоздать свое поведение описания для тестирования https://www.edaplayground.com/x/5QLs

Answer 2

Одно из возможных решений может быть достигнуто с помощью двух утверждений, как показано ниже.

Для 1-го изображения -

(req == fill) && (rsp == idle) |=> ((rsp == trans)[->1])[*4] 

для 2-го образа -

(req == fill) && (rsp == trans) |=> ((rsp == trans)[->1])[*0:4] ##1 (rsp == idle) ##1 ((rsp == trans)[->1])[*4] 

Одна проблема в том, что если есть непрерывное «заполнить» запросы на каждом цикле (последовательные 4 «заполнить» запросов, без любой промежуточный «простаивающий»), то второе утверждение не будет вычислять циклы «транс» для каждого запроса «заполнить» (вместо этого он будет завершен только во 2-м наборе «транс» циклов).

Я не мог изменить утверждение для данной ошибки, на данный момент.