Перейти к содержанию
    

System verilog assertion

Я пытаюсь добавлять в свои модули assertions и с последним выходит некрасиво.

 

REQ_ACK:
// hold req asserted until and including ack asserted
assert property ( @(posedge clk) disable iff(!rst_n)
    req |-> req[*1:$] ##0 ack
);

 

Я получаю сообщения:

Warning-[sVA-OPTCOV-LMFA] Large memory footprint assertion

test.v, 253

The assertion 'REQ_ACK' has the potential to consume a large amount of

memory.

Please examine the assertion for the use of large or unbounded delays and

repetitions.

Есть ли какие-нибудь способы переписать по-другому?

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Есть ли какие-нибудь способы переписать по-другому?

как бы правильное предупреждение, каждый такт, пока req == 1 вы будете рождать тред проверки. Почему бы вам не привязаться к фронту req например?

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Я пытаюсь добавлять в свои модули assertions и с последним выходит некрасиво.

 

REQ_ACK:
// hold req asserted until and including ack asserted
assert property ( @(posedge clk) disable iff(!rst_n)
    req |-> req[*1:$] ##0 ack
);

 

Я получаю сообщения:

 

Есть ли какие-нибудь способы переписать по-другому?

 

Я бы сказал, что lint'er/compiler ругается на Indefinite timing window, который собственно задается конструкцией типа [*1:$].

SVA Checker будет проверять это условие по каждому райзу клока, до конца симуляции, что и может повлечь большое использование памяти.

 

Поэтому "Eventuality Operator", коим является :$ не рекомендуют использовать без особой надобности, а писать хорошо определенные во времени assertions:

 

property p1;

@(posedge clk) a |-> ## [1:5] b ## [0: 2] c;

endproperty

 

a1: assert property (p1);

c1: cover property (p1); //Add to Functional Coverage Scoring

 

 

 

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

как бы правильное предупреждение, каждый такт, пока req == 1 вы будете рождать тред проверки. Почему бы вам не привязаться к фронту req например?

Да, но мне нужно чтобы req не опускался пока ack не поднимется.

 

писать хорошо определенные во времени assertions

Чтобы писать хорошо определенные во времени assertions нужно знать когда событие произойдет. А я не знаю. Может через клок, а может через 10000 или дольше.

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Задача - проверить, чтобы req не опускаля, пока ack не поднимется.

Если req переходит из 1 в 0 при ack==1, то можно обойтись таким свойством:

REQ_ACK:
// hold req asserted until and including ack asserted
cover property ( @(posedge clk) disable iff(!rst_n)
    req && !ack ||-> req
);

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Задача - проверить, чтобы req не опускаля, пока ack не поднимется.

Если req переходит из 1 в 0 при ack==1, то можно обойтись таким свойством:

REQ_ACK:
// hold req asserted until and including ack asserted
cover property ( @(posedge clk) disable iff(!rst_n)
    req && !ack ||-> req
);

hold req asserted until and including ack asserted - req должен быть поднят и во время ack. Он может и не опуститься потом.

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Тогда так:

REQ_ACK:
// hold req asserted until and including ack asserted
assert property ( @(posedge clk) disable iff(!rst_n)
    req |-> req[*1:max] ##0 ack
);

Приблизительное число тактов между запросами и ответами нужно все-таки знать. Его запихиваешь в max.

Для проверки делаешь еще 2 утверждения с директивой cover - считаешь количество посланных запросов и принятых ответов.

 

REQ_CNT: 
cover property ( @(posedge clk) disable iff(!rst_n)
    !req |=> req
);
RESP_CNT: 
cover property ( @(posedge clk) disable iff(!rst_n)
    !ack |=> ack
);

Если количество запросов и ответов в конце симуляции совпадает, а верхнее утверждение выдает ошибку, то нужно окно увеличивать (max).

 

Этот же вариант можно автоматизировать - завести 2 счетчика, которые будут считать запросы и ответы.

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

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Присоединяйтесь к обсуждению

Вы можете написать сейчас и зарегистрироваться позже. Если у вас есть аккаунт, авторизуйтесь, чтобы опубликовать от имени своего аккаунта.

Гость
Ответить в этой теме...

×   Вставлено с форматированием.   Вставить как обычный текст

  Разрешено использовать не более 75 эмодзи.

×   Ваша ссылка была автоматически встроена.   Отображать как обычную ссылку

×   Ваш предыдущий контент был восстановлен.   Очистить редактор

×   Вы не можете вставлять изображения напрямую. Загружайте или вставляйте изображения по ссылке.

×
×
  • Создать...