masics 0 1 мая, 2012 Опубликовано 1 мая, 2012 · Жалоба Я пытаюсь добавлять в свои модули 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. Есть ли какие-нибудь способы переписать по-другому? Цитата Поделиться сообщением Ссылка на сообщение Поделиться на другие сайты Поделиться
des00 25 1 мая, 2012 Опубликовано 1 мая, 2012 · Жалоба Есть ли какие-нибудь способы переписать по-другому? как бы правильное предупреждение, каждый такт, пока req == 1 вы будете рождать тред проверки. Почему бы вам не привязаться к фронту req например? Цитата Поделиться сообщением Ссылка на сообщение Поделиться на другие сайты Поделиться
mttphreak 0 3 мая, 2012 Опубликовано 3 мая, 2012 · Жалоба Я пытаюсь добавлять в свои модули 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 Цитата Поделиться сообщением Ссылка на сообщение Поделиться на другие сайты Поделиться
masics 0 3 мая, 2012 Опубликовано 3 мая, 2012 · Жалоба как бы правильное предупреждение, каждый такт, пока req == 1 вы будете рождать тред проверки. Почему бы вам не привязаться к фронту req например? Да, но мне нужно чтобы req не опускался пока ack не поднимется. писать хорошо определенные во времени assertions Чтобы писать хорошо определенные во времени assertions нужно знать когда событие произойдет. А я не знаю. Может через клок, а может через 10000 или дольше. Цитата Поделиться сообщением Ссылка на сообщение Поделиться на другие сайты Поделиться
lexus.mephi 0 3 мая, 2012 Опубликовано 3 мая, 2012 · Жалоба Задача - проверить, чтобы 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 ); Цитата Поделиться сообщением Ссылка на сообщение Поделиться на другие сайты Поделиться
masics 0 3 мая, 2012 Опубликовано 3 мая, 2012 · Жалоба Задача - проверить, чтобы 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. Он может и не опуститься потом. Цитата Поделиться сообщением Ссылка на сообщение Поделиться на другие сайты Поделиться
lexus.mephi 0 3 мая, 2012 Опубликовано 3 мая, 2012 · Жалоба Тогда так: 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, то выдаем ошибку (это можно в утверждении проверять). Цитата Поделиться сообщением Ссылка на сообщение Поделиться на другие сайты Поделиться