Свойства. Импликация.

Свойства

Свойства определяют отношение между логическими выражениями и последовательностями. Фактически, свойства описывают то, как будет проверяться выполнение последовательности или логического выражения:

• синхронно или асинхронно;
• не осуществлять проверку при наличии запрещающего сигнала (например, при активном сигнале сброса);
• осуществлять проверку только по условию (импликация).

В коде программы свойства описываются ключевыми словами property, endproperty:

property stable_addr;
@(posedge Clk) disable iff (~reset)
((CMD != `IDLE) && !CMD_ACCEPT) |=> $stable(ADDR);
endproperty 			

Свойство с именем stable_addr осуществляет проверку по переднему фронту тактового сигнала («@(posedge Clk)»). При активном сигнале reset проверка не выполняется («disable iff (~reset)»). Проверка того, что адрес не меняется, должна происходить только по событию. В данном случае событием является наличие команды на шине CMD. Для этого используется операция импликации.

Импликация (Implication)

Импликация очень часто применяется при построении утверждений. Это некое подобие оператора if. То, что слева оператора импликации, это условие. В качестве условия может быть булево выражение или последовательность. Если условие принимает значение истина, то начинает проверяться условие справа от значка импликации.
В SystemVerilog используется два вида импликации:

• перекрывающаяся («|->» – overlapped);
• неперекрывающаяся («|=>» – non-overlapped).

Рис. 15. а) Свойство с использованием перекрывающейся импликации; б) Свойство с использованием неперекрывающейся импликации

Если сравнить диаграммы на рис. 5 и рис. 15, то можно сделать вывод, что операторы «|->» и «|=>» эквивалентны задержкам в ##0 и ##1 тактов соответственно, но это не совсем так. Если в свойствах на рис. 15 заменить оператор «|->» на «##0», а оператор «|=>» на «##1», то в каждом такте будет проверяться, чтобы «a» было истинным. В этом случае для диаграмм, изображенных на рис. 15, свойства 1 и 2 при проверке на 2-4 тактах будут выдавать ошибки. Здесь целесообразно использовать импликацию, т.к. нам не нужно в каждом такте проверять истинность условия «a», нас интересует, чтобы условие «b» следовало за условием «a» только если «a» возникнет (станет истинным).
Справа от оператора импликации может использоваться конструкция «if/else». Предположим, у схемы, изображенной на рис. 1, есть режим «MODE1», в котором сигнал CMD_ACCEPT должен приходить только на следующем такте после появления на шине CMD команды. Во всех остальных режимах сигнал CMD_ACCEPT должен появляться в течение последующих трех тактов. С помощью конструкции «if/else» можно используя одно свойство осуществлять проверку генерации CMD_ACCEPT в режиме «MODE1» и в остальных режимах:

 property cmd_accept_wait;
    @(posedge Clk)
    (CMD != `IDLE) |->
        if (MODE1)
            (##1 CMD_ACCEPT)
        else
            (##[1:3] CMD_ACCEPT);
endproperty			

Свойства, как и последовательности, можно объединять с помощью логических операторов and и or. Помимо этого, в свойствах можно использовать логический оператор отрицания not:

 sequence seq1;
    a ##1 b;
endsequence
 
property not_seq1;
    @(posedge Clk) not seq1;
endproperty			

Это свойство на каждом такте проверяет, чтобы не выполнялась последовательность seq1.