Системные утверждения Verilog, SVA

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

свойство p1: @ (posedge clk) req ## [1: 5] ack; конечная собственность

свойство p2: @ (posedge clk) $ rose (ack) | -> $ past (req, 5);

Я не уверен, сохраняет ли это сопоставление «1 к 1» req vs ack.


system-verilog-assertions
person DeepG    schedule 13.02.2018    source источник

Ответы (3)


arrow_upward
0
arrow_downward

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

property p_test;
@(posedge clk)
$rose(req) |=> !req[*0:$] ##0 ack;
endproperty

Работает, если требуется только импульс

person Viktorinox    schedule 13.02.2018
comment
Привет, @Viktorinox, может быть несколько запросов подряд и одно за другим. Единственное условие - каждому запросу нужен соответствующий ack. - person DeepG; 06.03.2018

arrow_upward
0
arrow_downward

Свойство 2 ниже не синхронизировано со свойством 1.

свойство p2: @ (posedge clk) $ rose (ack) | -> $ past (req, 5);

Вы говорите, что у ack должен быть запрос на 5 часов раньше. Но свойство 1 говорит, что req, за которым следует ack, действительно.

Я думаю, вам нужен идентификатор с запросом, который вы можете сопоставить, когда произойдет подтверждение.

    sequence s_ack_check;
        byte id;
        (req && id == ack_id) ##[1:5](ack && ack_id == id);
    endsequence
person Sanjeev Singh    schedule 01.09.2019

arrow_upward
0
arrow_downward

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

Вот код, если вы хотите использовать вспомогательную логику:

Предположим, вы разрешили не более 15 выдающихся запросов, а для получения всех подтверждений требуется не более 25 тактов:

logic [3:0] req_cnt, ack_cnt;
always @ (posedge clk) if (rst) req_cnt <= 0; else req_cnt <= req_cnt + req;
always @ (posedge clk) if (rst) ack_cnt <= 0; else ack_cnt <= ack_cnt + ack;

assert property (@ (posedge clk) disable iff (rst) sync_accept_on(req) ##25 req_cnt == ack_cnt);

Подсчитайте запросы и подтверждения. Затем подтвердите, что после 25 циклов отсутствия запроса req_cnt == ack_cnt.

Если невыполненных запросов никогда не превышает 1, логика намного проще. Пожалуйста, поясните, так ли это.

person nachum    schedule 17.11.2019