Структура языка SVA

Язык SVA представляет некое подмножество языка SystemVerilog, что дает возможность применять метод верификации на основе SVA без полного изучения SystemVerilog. Семантика языка SVA схожа с PSL, но есть и ряд новых, по сравнению с языком PSL, возможностей.
Структура языка SVA нагляднее всего представляется, как показано на рис. 3. В основе любого SystemVerilog утверждения лежат булевы выражения, которые принимают значения ИСТИНА или ЛОЖЬ. В приведенном выше примере SystemVerilog утверждения используется два булевых выражения: «(CMD != `IDLE)» и «CMD_ACCEPT».

Рис. 3. Структура языка SVA

Последовательности описывают поведение проекта во времени и строятся на основе булевых выражений. Выражение «(CMD != `IDLE)» – это простая последовательность, состоящая из одного выражения. Сложные последовательности строятся с использованием временных задержек, которые задаются с помощью оператора «##»:

Рис. 4. Пример последовательности

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

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

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