Как написать свойство в утверждениях системы verilog?

Я хочу написать свойство в SVA, чтобы официально проверить поведение.Как написать свойство в утверждениях системы verilog?

Вот что я хочу:

property prop1(sig1,sig2,sig3,sig4); 
    @(posedge clk) 
    $fell(sig1) ##[1:$] first_match($fell(sig2)) ##0 sig3 |-> sig4 == sig3; 
endproperty

Как я могу переписать выше свойство, так что после sig1 падает, он остается низким в течение оставшихся циклов оценки?

Примечание: Я не хочу, чтобы положить sig1, как отключить IFF (sig1)

Спасибо!

источник

2016-05-06 kkdev

ли «после того, как sig1 падает, он остается низкий уровень в течение оставшихся циклов оценки», часть _precondition_ или _condition_? Другими словами, вы хотите проверить, что sig4 == sig3 _if_ sig1 остается низким ИЛИ вы хотите _check_, чтобы sig1 оставался низким, а также проверял sig4 = sig3? –

property prop1(sig1,sig2,sig3,sig4); 
    @(posedge clk) 
    (!sig1) throughout (##[1:$] first_match($fell(sig2)) ##0 sig3) 
      |-> sig4 == sig3; 
endproperty

См раздел 16.9.9 Условия над последовательностями в 1800-2012 LRM

источник

2016-05-06 17:03:01

Спасибо! Еще один запрос: как я могу расширить это свойство, чтобы проверить последовательную/удовлетворяющую последовательность в течение 16 последовательных циклов (sig4 == sig3) [* 16]? Также, убедившись, что sig1 == 1'b0; – kkdev

Вы также можете использовать ** во всем **, но в простом случае вы можете просто выполнить '(! Sig1 && sig4 == sig3) [* 16]' –

В приведенном выше случае, если sig1 является первичный ввод, тогда инструмент попытается найти контрпример, где sig1 равен 1'b1. Я попытался использовать «повсюду» в последующем, но не с успехом. Могу ли я попробовать что-то, как показано ниже? (! Sig1) во всем (## [1: $] first_match ($ fall (sig2)) ## 0 sig3 | -> sig4 == sig3) – kkdev

Как написать свойство в утверждениях системы verilog?

ответ

Смежные вопросы